vlsat3_b10.smt2 42.8 KB
Newer Older
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
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
(set-info :smt-lib-version 2.6)
(set-logic QF_DT)
(set-info :source |
Generated by: Pierre Bouvier
Generated on: 2021-03-12
Application: Automatic decomposition of Petri Nets into Automata Networks
Target solver: CVC4, Z3
Publications:

[1] Pierre Bouvier, Hubert Garavel, and Hernan Ponce de Leon.
    "Automatic Decomposition of Petri Nets into Automata Networks -
    A Synthetic Account". Proceedings PETRI NETS 2020, LNCS 12152,
    Springer. https://doi.org/10.1007/978-3-030-51831-8_1

[2] Hubert Garavel. "Nested-Unit Petri Nets". Journal of Logical
    and Algebraic Methods in Programming, vol. 104, Elsevier, 2019. 
    https://doi.org/10.1016/j.jlamp.2018.11.005

In [1], several methods for decomposing an ordinary, safe Petri net
into a flat, unit-safe NUPN [2], have been proposed. These methods
are implemented in a complete tool chain involving SAT solvers, SMT
solvers, and tools for graph coloring and finding maximal cliques.
From a data set of 12,000+ NUPN models, 51,000+ SMT formulas have
been generated, out of which a subset of 1200 interesting formulas
to be used as SMT-LIB 2.6 benchmarks was carefully selected.

Original filename: vlsat3_b10.smt2

Specific parameters for the present benchmark:
- number of places: 56
- number of units: 17
- number of edges in the concurrency graph: 1407
- number of variables: 56
- number of uninterpreted functions: 0
- number of asserts: 1423
- total number of operators in asserts: 4539
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unsat)

(declare-datatype Unit ((u0) (u1) (u2) (u3) (u4) (u5) (u6) (u7) (u8) (u9) (u10) (u11) (u12) (u13) (u14) (u15) (u16)))
(declare-fun p1 () Unit)
(declare-fun p2 () Unit)
(declare-fun p3 () Unit)
(declare-fun p4 () Unit)
(declare-fun p5 () Unit)
(declare-fun p6 () Unit)
(declare-fun p7 () Unit)
(declare-fun p8 () Unit)
(declare-fun p9 () Unit)
(declare-fun p10 () Unit)
(declare-fun p11 () Unit)
(declare-fun p12 () Unit)
(declare-fun p13 () Unit)
(declare-fun p14 () Unit)
(declare-fun p15 () Unit)
(declare-fun p16 () Unit)
(declare-fun p17 () Unit)
(declare-fun p18 () Unit)
(declare-fun p19 () Unit)
(declare-fun p20 () Unit)
(declare-fun p21 () Unit)
(declare-fun p22 () Unit)
(declare-fun p23 () Unit)
(declare-fun p24 () Unit)
(declare-fun p25 () Unit)
(declare-fun p26 () Unit)
(declare-fun p27 () Unit)
(declare-fun p28 () Unit)
(declare-fun p29 () Unit)
(declare-fun p30 () Unit)
(declare-fun p31 () Unit)
(declare-fun p32 () Unit)
(declare-fun p33 () Unit)
(declare-fun p34 () Unit)
(declare-fun p35 () Unit)
(declare-fun p36 () Unit)
(declare-fun p37 () Unit)
(declare-fun p38 () Unit)
(declare-fun p39 () Unit)
(declare-fun p40 () Unit)
(declare-fun p41 () Unit)
(declare-fun p42 () Unit)
(declare-fun p43 () Unit)
(declare-fun p44 () Unit)
(declare-fun p45 () Unit)
(declare-fun p46 () Unit)
(declare-fun p47 () Unit)
(declare-fun p48 () Unit)
(declare-fun p49 () Unit)
(declare-fun p50 () Unit)
(declare-fun p51 () Unit)
(declare-fun p52 () Unit)
(declare-fun p53 () Unit)
(declare-fun p54 () Unit)
(declare-fun p55 () Unit)
(declare-fun p56 () Unit)
(assert (= p1 u0))
(assert (or (= p2 u0) (= p2 u1)))
(assert (or (= p3 u0) (= p3 u1) (= p3 u2)))
(assert (or (= p4 u0) (= p4 u1) (= p4 u2) (= p4 u3)))
(assert (or (= p5 u0) (= p5 u1) (= p5 u2) (= p5 u3) (= p5 u4)))
(assert (or (= p6 u0) (= p6 u1) (= p6 u2) (= p6 u3) (= p6 u4) (= p6 u5)))
(assert (or (= p7 u0) (= p7 u1) (= p7 u2) (= p7 u3) (= p7 u4) (= p7 u5) (= p7 u6)))
(assert (or (= p8 u0) (= p8 u1) (= p8 u2) (= p8 u3) (= p8 u4) (= p8 u5) (= p8 u6) (= p8 u7)))
(assert (or (= p9 u0) (= p9 u1) (= p9 u2) (= p9 u3) (= p9 u4) (= p9 u5) (= p9 u6) (= p9 u7) (= p9 u8)))
(assert (or (= p10 u0) (= p10 u1) (= p10 u2) (= p10 u3) (= p10 u4) (= p10 u5) (= p10 u6) (= p10 u7) (= p10 u8) (= p10 u9)))
(assert (or (= p11 u0) (= p11 u1) (= p11 u2) (= p11 u3) (= p11 u4) (= p11 u5) (= p11 u6) (= p11 u7) (= p11 u8) (= p11 u9) (= p11 u10)))
(assert (or (= p12 u0) (= p12 u1) (= p12 u2) (= p12 u3) (= p12 u4) (= p12 u5) (= p12 u6) (= p12 u7) (= p12 u8) (= p12 u9) (= p12 u10) (= p12 u11)))
(assert (or (= p13 u0) (= p13 u1) (= p13 u2) (= p13 u3) (= p13 u4) (= p13 u5) (= p13 u6) (= p13 u7) (= p13 u8) (= p13 u9) (= p13 u10) (= p13 u11) (= p13 u12)))
(assert (or (= p14 u0) (= p14 u1) (= p14 u2) (= p14 u3) (= p14 u4) (= p14 u5) (= p14 u6) (= p14 u7) (= p14 u8) (= p14 u9) (= p14 u10) (= p14 u11) (= p14 u12) (= p14 u13)))
(assert (or (= p15 u0) (= p15 u1) (= p15 u2) (= p15 u3) (= p15 u4) (= p15 u5) (= p15 u6) (= p15 u7) (= p15 u8) (= p15 u9) (= p15 u10) (= p15 u11) (= p15 u12) (= p15 u13) (= p15 u14)))
(assert (or (= p16 u0) (= p16 u1) (= p16 u2) (= p16 u3) (= p16 u4) (= p16 u5) (= p16 u6) (= p16 u7) (= p16 u8) (= p16 u9) (= p16 u10) (= p16 u11) (= p16 u12) (= p16 u13) (= p16 u14) (= p16 u15)))
(assert (distinct p33 p55))
(assert (distinct p22 p29))
(assert (distinct p5 p37))
(assert (distinct p8 p26))
(assert (distinct p30 p45))
(assert (distinct p34 p42))
(assert (distinct p17 p48))
(assert (distinct p16 p31))
(assert (distinct p14 p21))
(assert (distinct p1 p56))
(assert (distinct p26 p50))
(assert (distinct p2 p41))
(assert (distinct p22 p38))
(assert (distinct p5 p36))
(assert (distinct p9 p39))
(assert (distinct p8 p23))
(assert (distinct p30 p38))
(assert (distinct p34 p35))
(assert (distinct p17 p39))
(assert (distinct p37 p42))
(assert (distinct p13 p51))
(assert (distinct p38 p55))
(assert (distinct p46 p55))
(assert (distinct p50 p52))
(assert (distinct p1 p15))
(assert (distinct p4 p12))
(assert (distinct p2 p34))
(assert (distinct p22 p47))
(assert (distinct p5 p43))
(assert (distinct p9 p46))
(assert (distinct p8 p16))
(assert (distinct p17 p30))
(assert (distinct p42 p44))
(assert (distinct p6 p54))
(assert (distinct p10 p51))
(assert (distinct p13 p42))
(assert (distinct p18 p51))
(assert (distinct p11 p20))
(assert (distinct p22 p56))
(assert (distinct p5 p18))
(assert (distinct p27 p35))
(assert (distinct p30 p56))
(assert (distinct p23 p31))
(assert (distinct p13 p33))
(assert (distinct p18 p44))
(assert (distinct p43 p54))
(assert (distinct p11 p27))
(assert (distinct p1 p29))
(assert (distinct p15 p39))
(assert (distinct p2 p52))
(assert (distinct p22 p49))
(assert (distinct p5 p25))
(assert (distinct p27 p46))
(assert (distinct p30 p49))
(assert (distinct p34 p54))
(assert (distinct p6 p40))
(assert (distinct p31 p50))
(assert (distinct p35 p45))
(assert (distinct p18 p45))
(assert (distinct p1 p20))
(assert (distinct p15 p42))
(assert (distinct p2 p53))
(assert (distinct p27 p53))
(assert (distinct p47 p52))
(assert (distinct p3 p46))
(assert (distinct p23 p41))
(assert (distinct p6 p33))
(assert (distinct p10 p38))
(assert (distinct p18 p38))
(assert (distinct p38 p43))
(assert (distinct p14 p50))
(assert (distinct p15 p49))
(assert (distinct p2 p14))
(assert (distinct p5 p15))
(assert (distinct p3 p37))
(assert (distinct p23 p36))
(assert (distinct p6 p42))
(assert (distinct p10 p47))
(assert (distinct p31 p36))
(assert (distinct p18 p31))
(assert (distinct p11 p56))
(assert (distinct p14 p43))
(assert (distinct p19 p56))
(assert (distinct p39 p51))
(assert (distinct p12 p29))
(assert (distinct p20 p30))
(assert (distinct p6 p19))
(assert (distinct p28 p46))
(assert (distinct p31 p43))
(assert (distinct p24 p26))
(assert (distinct p7 p52))
(assert (distinct p14 p36))
(assert (distinct p19 p47))
(assert (distinct p39 p54))
(assert (distinct p12 p22))
(assert (distinct p2 p32))
(assert (distinct p16 p34))
(assert (distinct p20 p35))
(assert (distinct p3 p55))
(assert (distinct p6 p28))
(assert (distinct p28 p35))
(assert (distinct p31 p46))
(assert (distinct p35 p49))
(assert (distinct p7 p43))
(assert (distinct p32 p55))
(assert (distinct p36 p52))
(assert (distinct p19 p42))
(assert (distinct p39 p45))
(assert (distinct p44 p52))
(assert (distinct p2 p17))
(assert (distinct p16 p47))
(assert (distinct p20 p44))
(assert (distinct p3 p50))
(assert (distinct p23 p53))
(assert (distinct p48 p53))
(assert (distinct p4 p51))
(assert (distinct p24 p48))
(assert (distinct p7 p46))
(assert (distinct p11 p33))
(assert (distinct p19 p33))
(assert (distinct p9 p23))
(assert (distinct p16 p56))
(assert (distinct p20 p49))
(assert (distinct p3 p9))
(assert (distinct p25 p38))
(assert (distinct p6 p14))
(assert (distinct p28 p49))
(assert (distinct p24 p37))
(assert (distinct p7 p37))
(assert (distinct p11 p44))
(assert (distinct p32 p37))
(assert (distinct p19 p28))
(assert (distinct p41 p53))
(assert (distinct p9 p30))
(assert (distinct p15 p24))
(assert (distinct p40 p54))
(assert (distinct p13 p26))
(assert (distinct p3 p4))
(assert (distinct p25 p45))
(assert (distinct p21 p25))
(assert (distinct p4 p33))
(assert (distinct p7 p32))
(assert (distinct p29 p41))
(assert (distinct p33 p44))
(assert (distinct p32 p46))
(assert (distinct p8 p53))
(assert (distinct p12 p50))
(assert (distinct p15 p31))
(assert (distinct p40 p51))
(assert (distinct p13 p17))
(assert (distinct p3 p27))
(assert (distinct p25 p52))
(assert (distinct p1 p45))
(assert (distinct p21 p40))
(assert (distinct p4 p42))
(assert (distinct p7 p23))
(assert (distinct p29 p40))
(assert (distinct p33 p35))
(assert (distinct p32 p43))
(assert (distinct p36 p48))
(assert (distinct p9 p12))
(assert (distinct p8 p46))
(assert (distinct p12 p55))
(assert (distinct p37 p55))
(assert (distinct p40 p44))
(assert (distinct p45 p55))
(assert (distinct p49 p50))
(assert (distinct p3 p22))
(assert (distinct p1 p36))
(assert (distinct p21 p47))
(assert (distinct p4 p47))
(assert (distinct p24 p52))
(assert (distinct p7 p10))
(assert (distinct p41 p42))
(assert (distinct p5 p56))
(assert (distinct p9 p51))
(assert (distinct p8 p43))
(assert (distinct p12 p48))
(assert (distinct p17 p51))
(assert (distinct p45 p46))
(assert (distinct p10 p22))
(assert (distinct p21 p54))
(assert (distinct p4 p24))
(assert (distinct p26 p39))
(assert (distinct p29 p54))
(assert (distinct p33 p49))
(assert (distinct p8 p36))
(assert (distinct p12 p37))
(assert (distinct p17 p42))
(assert (distinct p42 p56))
(assert (distinct p10 p31))
(assert (distinct p16 p17))
(assert (distinct p14 p27))
(assert (distinct p1 p50))
(assert (distinct p4 p29))
(assert (distinct p26 p48))
(assert (distinct p33 p56))
(assert (distinct p22 p28))
(assert (distinct p5 p38))
(assert (distinct p9 p33))
(assert (distinct p8 p25))
(assert (distinct p30 p44))
(assert (distinct p34 p41))
(assert (distinct p17 p33))
(assert (distinct p13 p53))
(assert (distinct p16 p26))
(assert (distinct p14 p20))
(assert (distinct p1 p9))
(assert (distinct p26 p49))
(assert (distinct p2 p48))
(assert (distinct p22 p37))
(assert (distinct p5 p45))
(assert (distinct p9 p40))
(assert (distinct p8 p18))
(assert (distinct p30 p37))
(assert (distinct p17 p40))
(assert (distinct p37 p43))
(assert (distinct p13 p52))
(assert (distinct p38 p54))
(assert (distinct p46 p54))
(assert (distinct p50 p51))
(assert (distinct p1 p16))
(assert (distinct p4 p11))
(assert (distinct p2 p33))
(assert (distinct p22 p46))
(assert (distinct p5 p44))
(assert (distinct p9 p47))
(assert (distinct p8 p15))
(assert (distinct p17 p31))
(assert (distinct p42 p43))
(assert (distinct p6 p53))
(assert (distinct p10 p50))
(assert (distinct p13 p43))
(assert (distinct p18 p50))
(assert (distinct p46 p47))
(assert (distinct p11 p17))
(assert (distinct p22 p55))
(assert (distinct p5 p19))
(assert (distinct p27 p36))
(assert (distinct p30 p55))
(assert (distinct p34 p52))
(assert (distinct p23 p32))
(assert (distinct p13 p34))
(assert (distinct p18 p43))
(assert (distinct p43 p51))
(assert (distinct p11 p28))
(assert (distinct p1 p30))
(assert (distinct p15 p40))
(assert (distinct p2 p51))
(assert (distinct p5 p26))
(assert (distinct p27 p43))
(assert (distinct p34 p53))
(assert (distinct p6 p39))
(assert (distinct p10 p36))
(assert (distinct p31 p55))
(assert (distinct p35 p46))
(assert (distinct p18 p36))
(assert (distinct p14 p56))
(assert (distinct p1 p21))
(assert (distinct p15 p47))
(assert (distinct p2 p12))
(assert (distinct p27 p54))
(assert (distinct p47 p49))
(assert (distinct p3 p43))
(assert (distinct p23 p42))
(assert (distinct p6 p48))
(assert (distinct p10 p37))
(assert (distinct p18 p37))
(assert (distinct p38 p42))
(assert (distinct p14 p49))
(assert (distinct p15 p50))
(assert (distinct p2 p13))
(assert (distinct p5 p16))
(assert (distinct p3 p38))
(assert (distinct p23 p33))
(assert (distinct p6 p41))
(assert (distinct p10 p46))
(assert (distinct p31 p33))
(assert (distinct p18 p30))
(assert (distinct p11 p53))
(assert (distinct p14 p42))
(assert (distinct p19 p53))
(assert (distinct p39 p52))
(assert (distinct p12 p32))
(assert (distinct p20 p29))
(assert (distinct p6 p18))
(assert (distinct p28 p45))
(assert (distinct p31 p44))
(assert (distinct p35 p55))
(assert (distinct p24 p25))
(assert (distinct p7 p49))
(assert (distinct p14 p35))
(assert (distinct p19 p48))
(assert (distinct p39 p43))
(assert (distinct p12 p21))
(assert (distinct p2 p31))
(assert (distinct p16 p33))
(assert (distinct p20 p38))
(assert (distinct p3 p56))
(assert (distinct p23 p51))
(assert (distinct p6 p27))
(assert (distinct p28 p38))
(assert (distinct p35 p50))
(assert (distinct p7 p44))
(assert (distinct p11 p39))
(assert (distinct p32 p50))
(assert (distinct p36 p51))
(assert (distinct p19 p39))
(assert (distinct p39 p46))
(assert (distinct p44 p51))
(assert (distinct p9 p17))
(assert (distinct p2 p24))
(assert (distinct p16 p42))
(assert (distinct p20 p43))
(assert (distinct p3 p15))
(assert (distinct p23 p54))
(assert (distinct p48 p56))
(assert (distinct p4 p54))
(assert (distinct p24 p47))
(assert (distinct p7 p35))
(assert (distinct p11 p34))
(assert (distinct p19 p34))
(assert (distinct p9 p24))
(assert (distinct p16 p55))
(assert (distinct p20 p52))
(assert (distinct p3 p10))
(assert (distinct p25 p39))
(assert (distinct p6 p13))
(assert (distinct p28 p52))
(assert (distinct p24 p40))
(assert (distinct p7 p38))
(assert (distinct p11 p41))
(assert (distinct p32 p40))
(assert (distinct p19 p25))
(assert (distinct p41 p54))
(assert (distinct p9 p31))
(assert (distinct p15 p21))
(assert (distinct p40 p53))
(assert (distinct p27 p28))
(assert (distinct p13 p27))
(assert (distinct p25 p46))
(assert (distinct p21 p26))
(assert (distinct p4 p36))
(assert (distinct p7 p29))
(assert (distinct p29 p42))
(assert (distinct p33 p45))
(assert (distinct p32 p45))
(assert (distinct p36 p42))
(assert (distinct p19 p20))
(assert (distinct p8 p56))
(assert (distinct p12 p49))
(assert (distinct p15 p32))
(assert (distinct p40 p46))
(assert (distinct p13 p18))
(assert (distinct p3 p28))
(assert (distinct p25 p53))
(assert (distinct p1 p46))
(assert (distinct p21 p33))
(assert (distinct p4 p41))
(assert (distinct p24 p54))
(assert (distinct p7 p24))
(assert (distinct p29 p33))
(assert (distinct p33 p36))
(assert (distinct p36 p47))
(assert (distinct p8 p45))
(assert (distinct p12 p42))
(assert (distinct p37 p56))
(assert (distinct p40 p43))
(assert (distinct p45 p56))
(assert (distinct p10 p20))
(assert (distinct p49 p51))
(assert (distinct p3 p19))
(assert (distinct p1 p37))
(assert (distinct p21 p48))
(assert (distinct p4 p18))
(assert (distinct p24 p51))
(assert (distinct p7 p15))
(assert (distinct p41 p43))
(assert (distinct p5 p49))
(assert (distinct p9 p52))
(assert (distinct p8 p38))
(assert (distinct p12 p47))
(assert (distinct p17 p52))
(assert (distinct p45 p47))
(assert (distinct p10 p21))
(assert (distinct p21 p55))
(assert (distinct p4 p23))
(assert (distinct p26 p38))
(assert (distinct p29 p55))
(assert (distinct p33 p50))
(assert (distinct p8 p35))
(assert (distinct p12 p40))
(assert (distinct p17 p43))
(assert (distinct p37 p38))
(assert (distinct p42 p55))
(assert (distinct p10 p30))
(assert (distinct p16 p20))
(assert (distinct p14 p26))
(assert (distinct p1 p51))
(assert (distinct p4 p32))
(assert (distinct p26 p47))
(assert (distinct p22 p27))
(assert (distinct p5 p39))
(assert (distinct p9 p34))
(assert (distinct p8 p28))
(assert (distinct p30 p43))
(assert (distinct p34 p48))
(assert (distinct p17 p34))
(assert (distinct p37 p45))
(assert (distinct p13 p54))
(assert (distinct p16 p25))
(assert (distinct p14 p19))
(assert (distinct p1 p10))
(assert (distinct p26 p56))
(assert (distinct p2 p47))
(assert (distinct p22 p36))
(assert (distinct p5 p46))
(assert (distinct p9 p41))
(assert (distinct p8 p17))
(assert (distinct p30 p36))
(assert (distinct p17 p25))
(assert (distinct p37 p44))
(assert (distinct p13 p45))
(assert (distinct p38 p53))
(assert (distinct p46 p53))
(assert (distinct p11 p23))
(assert (distinct p4 p14))
(assert (distinct p2 p40))
(assert (distinct p22 p45))
(assert (distinct p5 p21))
(assert (distinct p9 p48))
(assert (distinct p8 p10))
(assert (distinct p17 p32))
(assert (distinct p6 p52))
(assert (distinct p10 p49))
(assert (distinct p13 p44))
(assert (distinct p18 p49))
(assert (distinct p11 p18))
(assert (distinct p22 p54))
(assert (distinct p5 p20))
(assert (distinct p27 p33))
(assert (distinct p30 p54))
(assert (distinct p34 p51))
(assert (distinct p23 p29))
(assert (distinct p13 p35))
(assert (distinct p18 p42))
(assert (distinct p38 p39))
(assert (distinct p43 p52))
(assert (distinct p11 p25))
(assert (distinct p1 p31))
(assert (distinct p15 p37))
(assert (distinct p2 p50))
(assert (distinct p5 p27))
(assert (distinct p27 p44))
(assert (distinct p6 p38))
(assert (distinct p10 p35))
(assert (distinct p31 p56))
(assert (distinct p35 p43))
(assert (distinct p18 p35))
(assert (distinct p38 p48))
(assert (distinct p14 p55))
(assert (distinct p1 p22))
(assert (distinct p15 p48))
(assert (distinct p2 p11))
(assert (distinct p27 p51))
(assert (distinct p47 p50))
(assert (distinct p3 p44))
(assert (distinct p23 p47))
(assert (distinct p6 p47))
(assert (distinct p10 p44))
(assert (distinct p18 p28))
(assert (distinct p38 p41))
(assert (distinct p14 p48))
(assert (distinct p12 p26))
(assert (distinct p15 p55))
(assert (distinct p2 p4))
(assert (distinct p5 p9))
(assert (distinct p3 p35))
(assert (distinct p23 p34))
(assert (distinct p6 p24))
(assert (distinct p10 p45))
(assert (distinct p31 p34))
(assert (distinct p18 p29))
(assert (distinct p11 p54))
(assert (distinct p14 p41))
(assert (distinct p19 p54))
(assert (distinct p39 p49))
(assert (distinct p12 p31))
(assert (distinct p20 p32))
(assert (distinct p6 p17))
(assert (distinct p28 p48))
(assert (distinct p31 p41))
(assert (distinct p35 p56))
(assert (distinct p24 p28))
(assert (distinct p7 p50))
(assert (distinct p14 p34))
(assert (distinct p19 p45))
(assert (distinct p39 p44))
(assert (distinct p12 p24))
(assert (distinct p2 p30))
(assert (distinct p16 p36))
(assert (distinct p20 p37))
(assert (distinct p3 p53))
(assert (distinct p23 p52))
(assert (distinct p6 p26))
(assert (distinct p28 p37))
(assert (distinct p7 p41))
(assert (distinct p11 p40))
(assert (distinct p32 p49))
(assert (distinct p36 p54))
(assert (distinct p19 p40))
(assert (distinct p44 p54))
(assert (distinct p9 p18))
(assert (distinct p2 p23))
(assert (distinct p16 p41))
(assert (distinct p20 p46))
(assert (distinct p3 p16))
(assert (distinct p25 p33))
(assert (distinct p48 p55))
(assert (distinct p4 p53))
(assert (distinct p24 p42))
(assert (distinct p7 p36))
(assert (distinct p11 p47))
(assert (distinct p19 p31))
(assert (distinct p9 p25))
(assert (distinct p15 p19))
(assert (distinct p13 p29))
(assert (distinct p16 p50))
(assert (distinct p20 p51))
(assert (distinct p25 p40))
(assert (distinct p6 p12))
(assert (distinct p28 p51))
(assert (distinct p24 p39))
(assert (distinct p7 p27))
(assert (distinct p11 p42))
(assert (distinct p32 p39))
(assert (distinct p19 p26))
(assert (distinct p41 p55))
(assert (distinct p9 p32))
(assert (distinct p15 p22))
(assert (distinct p40 p56))
(assert (distinct p13 p28))
(assert (distinct p25 p47))
(assert (distinct p21 p27))
(assert (distinct p4 p35))
(assert (distinct p7 p30))
(assert (distinct p29 p43))
(assert (distinct p33 p46))
(assert (distinct p32 p48))
(assert (distinct p36 p41))
(assert (distinct p8 p55))
(assert (distinct p12 p52))
(assert (distinct p15 p29))
(assert (distinct p40 p45))
(assert (distinct p13 p19))
(assert (distinct p3 p25))
(assert (distinct p25 p54))
(assert (distinct p1 p47))
(assert (distinct p21 p34))
(assert (distinct p4 p44))
(assert (distinct p24 p53))
(assert (distinct p7 p21))
(assert (distinct p29 p34))
(assert (distinct p8 p48))
(assert (distinct p12 p41))
(assert (distinct p37 p49))
(assert (distinct p45 p49))
(assert (distinct p10 p19))
(assert (distinct p49 p52))
(assert (distinct p3 p20))
(assert (distinct p1 p38))
(assert (distinct p21 p41))
(assert (distinct p4 p17))
(assert (distinct p26 p36))
(assert (distinct p7 p16))
(assert (distinct p41 p44))
(assert (distinct p5 p50))
(assert (distinct p9 p53))
(assert (distinct p8 p37))
(assert (distinct p12 p34))
(assert (distinct p17 p53))
(assert (distinct p10 p28))
(assert (distinct p16 p22))
(assert (distinct p14 p32))
(assert (distinct p21 p56))
(assert (distinct p4 p26))
(assert (distinct p26 p37))
(assert (distinct p29 p56))
(assert (distinct p33 p51))
(assert (distinct p8 p30))
(assert (distinct p12 p39))
(assert (distinct p17 p44))
(assert (distinct p37 p39))
(assert (distinct p42 p54))
(assert (distinct p10 p29))
(assert (distinct p16 p19))
(assert (distinct p14 p25))
(assert (distinct p1 p52))
(assert (distinct p4 p31))
(assert (distinct p26 p46))
(assert (distinct p22 p26))
(assert (distinct p5 p40))
(assert (distinct p9 p35))
(assert (distinct p8 p27))
(assert (distinct p30 p42))
(assert (distinct p34 p47))
(assert (distinct p17 p35))
(assert (distinct p37 p46))
(assert (distinct p13 p55))
(assert (distinct p16 p28))
(assert (distinct p14 p18))
(assert (distinct p1 p11))
(assert (distinct p26 p55))
(assert (distinct p2 p46))
(assert (distinct p22 p35))
(assert (distinct p5 p47))
(assert (distinct p9 p42))
(assert (distinct p8 p20))
(assert (distinct p30 p35))
(assert (distinct p17 p26))
(assert (distinct p13 p46))
(assert (distinct p38 p52))
(assert (distinct p46 p52))
(assert (distinct p11 p24))
(assert (distinct p1 p2))
(assert (distinct p4 p13))
(assert (distinct p2 p39))
(assert (distinct p22 p44))
(assert (distinct p5 p22))
(assert (distinct p27 p39))
(assert (distinct p8 p9))
(assert (distinct p23 p27))
(assert (distinct p6 p51))
(assert (distinct p10 p56))
(assert (distinct p13 p37))
(assert (distinct p18 p56))
(assert (distinct p11 p31))
(assert (distinct p1 p25))
(assert (distinct p15 p35))
(assert (distinct p22 p53))
(assert (distinct p5 p29))
(assert (distinct p27 p34))
(assert (distinct p30 p53))
(assert (distinct p34 p50))
(assert (distinct p23 p30))
(assert (distinct p13 p36))
(assert (distinct p18 p41))
(assert (distinct p43 p49))
(assert (distinct p11 p26))
(assert (distinct p1 p32))
(assert (distinct p15 p38))
(assert (distinct p2 p49))
(assert (distinct p5 p28))
(assert (distinct p27 p41))
(assert (distinct p6 p37))
(assert (distinct p10 p34))
(assert (distinct p31 p53))
(assert (distinct p35 p44))
(assert (distinct p18 p34))
(assert (distinct p38 p47))
(assert (distinct p14 p54))
(assert (distinct p1 p23))
(assert (distinct p15 p45))
(assert (distinct p2 p10))
(assert (distinct p27 p52))
(assert (distinct p47 p55))
(assert (distinct p3 p41))
(assert (distinct p23 p48))
(assert (distinct p6 p46))
(assert (distinct p10 p43))
(assert (distinct p18 p27))
(assert (distinct p11 p12))
(assert (distinct p14 p47))
(assert (distinct p26 p28))
(assert (distinct p12 p25))
(assert (distinct p15 p56))
(assert (distinct p2 p3))
(assert (distinct p5 p10))
(assert (distinct p20 p26))
(assert (distinct p3 p36))
(assert (distinct p23 p39))
(assert (distinct p6 p23))
(assert (distinct p28 p42))
(assert (distinct p31 p39))
(assert (distinct p18 p20))
(assert (distinct p24 p30))
(assert (distinct p11 p51))
(assert (distinct p14 p40))
(assert (distinct p19 p51))
(assert (distinct p39 p50))
(assert (distinct p12 p18))
(assert (distinct p2 p28))
(assert (distinct p16 p38))
(assert (distinct p20 p31))
(assert (distinct p6 p32))
(assert (distinct p28 p47))
(assert (distinct p31 p42))
(assert (distinct p35 p53))
(assert (distinct p24 p27))
(assert (distinct p7 p55))
(assert (distinct p14 p33))
(assert (distinct p19 p46))
(assert (distinct p39 p41))
(assert (distinct p12 p23))
(assert (distinct p2 p29))
(assert (distinct p16 p35))
(assert (distinct p20 p40))
(assert (distinct p3 p54))
(assert (distinct p23 p49))
(assert (distinct p6 p25))
(assert (distinct p28 p40))
(assert (distinct p7 p42))
(assert (distinct p11 p37))
(assert (distinct p32 p52))
(assert (distinct p36 p53))
(assert (distinct p19 p37))
(assert (distinct p44 p53))
(assert (distinct p9 p19))
(assert (distinct p2 p22))
(assert (distinct p16 p44))
(assert (distinct p20 p45))
(assert (distinct p3 p13))
(assert (distinct p25 p34))
(assert (distinct p48 p50))
(assert (distinct p21 p22))
(assert (distinct p4 p56))
(assert (distinct p24 p41))
(assert (distinct p7 p33))
(assert (distinct p11 p48))
(assert (distinct p19 p32))
(assert (distinct p41 p49))
(assert (distinct p9 p26))
(assert (distinct p15 p20))
(assert (distinct p13 p30))
(assert (distinct p16 p49))
(assert (distinct p20 p54))
(assert (distinct p25 p41))
(assert (distinct p6 p11))
(assert (distinct p28 p54))
(assert (distinct p21 p29))
(assert (distinct p24 p34))
(assert (distinct p7 p28))
(assert (distinct p29 p45))
(assert (distinct p32 p34))
(assert (distinct p41 p56))
(assert (distinct p15 p27))
(assert (distinct p40 p55))
(assert (distinct p13 p21))
(assert (distinct p3 p31))
(assert (distinct p25 p48))
(assert (distinct p1 p41))
(assert (distinct p21 p28))
(assert (distinct p4 p38))
(assert (distinct p7 p19))
(assert (distinct p29 p44))
(assert (distinct p33 p47))
(assert (distinct p32 p47))
(assert (distinct p36 p44))
(assert (distinct p8 p50))
(assert (distinct p12 p51))
(assert (distinct p15 p30))
(assert (distinct p40 p48))
(assert (distinct p13 p20))
(assert (distinct p3 p26))
(assert (distinct p25 p55))
(assert (distinct p1 p48))
(assert (distinct p21 p35))
(assert (distinct p4 p43))
(assert (distinct p24 p56))
(assert (distinct p7 p22))
(assert (distinct p29 p35))
(assert (distinct p8 p47))
(assert (distinct p12 p44))
(assert (distinct p37 p50))
(assert (distinct p45 p50))
(assert (distinct p10 p18))
(assert (distinct p3 p17))
(assert (distinct p1 p39))
(assert (distinct p21 p42))
(assert (distinct p4 p20))
(assert (distinct p26 p35))
(assert (distinct p7 p13))
(assert (distinct p22 p23))
(assert (distinct p5 p51))
(assert (distinct p9 p54))
(assert (distinct p8 p40))
(assert (distinct p12 p33))
(assert (distinct p17 p54))
(assert (distinct p42 p52))
(assert (distinct p10 p27))
(assert (distinct p16 p21))
(assert (distinct p14 p31))
(assert (distinct p21 p49))
(assert (distinct p4 p25))
(assert (distinct p26 p44))
(assert (distinct p29 p49))
(assert (distinct p33 p52))
(assert (distinct p22 p32))
(assert (distinct p8 p29))
(assert (distinct p30 p48))
(assert (distinct p17 p45))
(assert (distinct p42 p53))
(assert (distinct p16 p30))
(assert (distinct p14 p24))
(assert (distinct p1 p53))
(assert (distinct p26 p45))
(assert (distinct p2 p44))
(assert (distinct p22 p25))
(assert (distinct p5 p33))
(assert (distinct p9 p36))
(assert (distinct p8 p22))
(assert (distinct p30 p41))
(assert (distinct p34 p46))
(assert (distinct p17 p36))
(assert (distinct p37 p47))
(assert (distinct p13 p56))
(assert (distinct p16 p27))
(assert (distinct p14 p17))
(assert (distinct p1 p12))
(assert (distinct p26 p54))
(assert (distinct p2 p45))
(assert (distinct p22 p34))
(assert (distinct p5 p48))
(assert (distinct p9 p43))
(assert (distinct p8 p19))
(assert (distinct p30 p34))
(assert (distinct p17 p27))
(assert (distinct p13 p47))
(assert (distinct p38 p51))
(assert (distinct p25 p26))
(assert (distinct p46 p51))
(assert (distinct p11 p21))
(assert (distinct p1 p3))
(assert (distinct p4 p16))
(assert (distinct p29 p30))
(assert (distinct p2 p38))
(assert (distinct p22 p43))
(assert (distinct p5 p23))
(assert (distinct p27 p40))
(assert (distinct p8 p12))
(assert (distinct p17 p18))
(assert (distinct p23 p28))
(assert (distinct p6 p50))
(assert (distinct p10 p55))
(assert (distinct p13 p38))
(assert (distinct p18 p55))
(assert (distinct p43 p55))
(assert (distinct p11 p32))
(assert (distinct p1 p26))
(assert (distinct p15 p36))
(assert (distinct p22 p52))
(assert (distinct p5 p30))
(assert (distinct p27 p47))
(assert (distinct p30 p52))
(assert (distinct p34 p49))
(assert (distinct p31 p51))
(assert (distinct p18 p48))
(assert (distinct p43 p50))
(assert (distinct p1 p17))
(assert (distinct p15 p43))
(assert (distinct p2 p56))
(assert (distinct p27 p42))
(assert (distinct p3 p47))
(assert (distinct p6 p36))
(assert (distinct p10 p33))
(assert (distinct p31 p54))
(assert (distinct p35 p41))
(assert (distinct p18 p33))
(assert (distinct p38 p46))
(assert (distinct p14 p53))
(assert (distinct p1 p24))
(assert (distinct p15 p46))
(assert (distinct p2 p9))
(assert (distinct p27 p49))
(assert (distinct p47 p56))
(assert (distinct p3 p42))
(assert (distinct p23 p45))
(assert (distinct p6 p45))
(assert (distinct p10 p42))
(assert (distinct p35 p36))
(assert (distinct p18 p26))
(assert (distinct p14 p46))
(assert (distinct p26 p27))
(assert (distinct p12 p28))
(assert (distinct p15 p53))
(assert (distinct p5 p11))
(assert (distinct p30 p31))
(assert (distinct p20 p25))
(assert (distinct p3 p33))
(assert (distinct p23 p40))
(assert (distinct p6 p22))
(assert (distinct p28 p41))
(assert (distinct p31 p40))
(assert (distinct p18 p19))
(assert (distinct p24 p29))
(assert (distinct p11 p52))
(assert (distinct p14 p39))
(assert (distinct p19 p52))
(assert (distinct p39 p55))
(assert (distinct p12 p17))
(assert (distinct p2 p27))
(assert (distinct p16 p37))
(assert (distinct p20 p34))
(assert (distinct p6 p31))
(assert (distinct p28 p34))
(assert (distinct p31 p47))
(assert (distinct p35 p54))
(assert (distinct p7 p56))
(assert (distinct p32 p54))
(assert (distinct p19 p43))
(assert (distinct p39 p42))
(assert (distinct p2 p20))
(assert (distinct p16 p46))
(assert (distinct p20 p39))
(assert (distinct p3 p51))
(assert (distinct p23 p50))
(assert (distinct p28 p39))
(assert (distinct p4 p50))
(assert (distinct p7 p47))
(assert (distinct p11 p38))
(assert (distinct p32 p51))
(assert (distinct p36 p56))
(assert (distinct p19 p38))
(assert (distinct p44 p56))
(assert (distinct p9 p20))
(assert (distinct p2 p21))
(assert (distinct p16 p43))
(assert (distinct p20 p48))
(assert (distinct p3 p14))
(assert (distinct p25 p35))
(assert (distinct p48 p49))
(assert (distinct p21 p23))
(assert (distinct p4 p55))
(assert (distinct p24 p44))
(assert (distinct p7 p34))
(assert (distinct p11 p45))
(assert (distinct p19 p29))
(assert (distinct p41 p50))
(assert (distinct p9 p27))
(assert (distinct p15 p17))
(assert (distinct p13 p31))
(assert (distinct p16 p52))
(assert (distinct p20 p53))
(assert (distinct p25 p42))
(assert (distinct p6 p10))
(assert (distinct p28 p53))
(assert (distinct p21 p30))
(assert (distinct p24 p33))
(assert (distinct p7 p25))
(assert (distinct p29 p46))
(assert (distinct p33 p41))
(assert (distinct p32 p33))
(assert (distinct p15 p28))
(assert (distinct p40 p50))
(assert (distinct p13 p22))
(assert (distinct p3 p32))
(assert (distinct p25 p49))
(assert (distinct p1 p42))
(assert (distinct p21 p37))
(assert (distinct p4 p37))
(assert (distinct p7 p20))
(assert (distinct p29 p37))
(assert (distinct p33 p48))
(assert (distinct p32 p42))
(assert (distinct p36 p43))
(assert (distinct p8 p49))
(assert (distinct p12 p54))
(assert (distinct p40 p47))
(assert (distinct p3 p23))
(assert (distinct p25 p56))
(assert (distinct p1 p33))
(assert (distinct p21 p36))
(assert (distinct p4 p46))
(assert (distinct p24 p55))
(assert (distinct p7 p11))
(assert (distinct p29 p36))
(assert (distinct p5 p53))
(assert (distinct p8 p42))
(assert (distinct p12 p43))
(assert (distinct p37 p51))
(assert (distinct p45 p51))
(assert (distinct p10 p17))
(assert (distinct p3 p18))
(assert (distinct p1 p40))
(assert (distinct p21 p43))
(assert (distinct p4 p19))
(assert (distinct p26 p34))
(assert (distinct p7 p14))
(assert (distinct p5 p52))
(assert (distinct p9 p55))
(assert (distinct p8 p39))
(assert (distinct p12 p36))
(assert (distinct p17 p55))
(assert (distinct p42 p51))
(assert (distinct p10 p26))
(assert (distinct p16 p24))
(assert (distinct p14 p30))
(assert (distinct p21 p50))
(assert (distinct p4 p28))
(assert (distinct p26 p43))
(assert (distinct p29 p50))
(assert (distinct p33 p53))
(assert (distinct p22 p31))
(assert (distinct p8 p32))
(assert (distinct p30 p47))
(assert (distinct p34 p44))
(assert (distinct p17 p46))
(assert (distinct p16 p29))
(assert (distinct p14 p23))
(assert (distinct p1 p54))
(assert (distinct p26 p52))
(assert (distinct p2 p43))
(assert (distinct p22 p40))
(assert (distinct p5 p34))
(assert (distinct p9 p37))
(assert (distinct p8 p21))
(assert (distinct p30 p40))
(assert (distinct p34 p45))
(assert (distinct p17 p37))
(assert (distinct p37 p48))
(assert (distinct p10 p12))
(assert (distinct p13 p49))
(assert (distinct p1 p13))
(assert (distinct p4 p10))
(assert (distinct p26 p53))
(assert (distinct p2 p36))
(assert (distinct p22 p33))
(assert (distinct p5 p41))
(assert (distinct p9 p44))
(assert (distinct p8 p14))
(assert (distinct p30 p33))
(assert (distinct p17 p28))
(assert (distinct p6 p56))
(assert (distinct p13 p48))
(assert (distinct p38 p50))
(assert (distinct p25 p27))
(assert (distinct p46 p50))
(assert (distinct p11 p22))
(assert (distinct p1 p4))
(assert (distinct p4 p15))
(assert (distinct p29 p31))
(assert (distinct p2 p37))
(assert (distinct p22 p42))
(assert (distinct p5 p24))
(assert (distinct p27 p37))
(assert (distinct p8 p11))
(assert (distinct p17 p19))
(assert (distinct p23 p25))
(assert (distinct p6 p49))
(assert (distinct p10 p54))
(assert (distinct p13 p39))
(assert (distinct p18 p54))
(assert (distinct p43 p56))
(assert (distinct p11 p29))
(assert (distinct p1 p27))
(assert (distinct p15 p33))
(assert (distinct p22 p51))
(assert (distinct p5 p31))
(assert (distinct p27 p48))
(assert (distinct p30 p51))
(assert (distinct p34 p56))
(assert (distinct p31 p52))
(assert (distinct p35 p47))
(assert (distinct p18 p47))
(assert (distinct p1 p18))
(assert (distinct p15 p44))
(assert (distinct p2 p55))
(assert (distinct p5 p6))
(assert (distinct p27 p55))
(assert (distinct p3 p48))
(assert (distinct p23 p43))
(assert (distinct p6 p35))
(assert (distinct p10 p40))
(assert (distinct p35 p42))
(assert (distinct p18 p40))
(assert (distinct p38 p45))
(assert (distinct p14 p52))
(assert (distinct p15 p51))
(assert (distinct p2 p16))
(assert (distinct p5 p13))
(assert (distinct p27 p50))
(assert (distinct p47 p53))
(assert (distinct p3 p39))
(assert (distinct p23 p46))
(assert (distinct p6 p44))
(assert (distinct p10 p41))
(assert (distinct p18 p25))
(assert (distinct p14 p45))
(assert (distinct p12 p27))
(assert (distinct p51 p52))
(assert (distinct p15 p54))
(assert (distinct p5 p12))
(assert (distinct p20 p28))
(assert (distinct p3 p34))
(assert (distinct p23 p37))
(assert (distinct p6 p21))
(assert (distinct p28 p44))
(assert (distinct p31 p37))
(assert (distinct p43 p44))
(assert (distinct p24 p32))
(assert (distinct p11 p49))
(assert (distinct p14 p38))
(assert (distinct p19 p49))
(assert (distinct p39 p56))
(assert (distinct p12 p20))
(assert (distinct p2 p26))
(assert (distinct p16 p40))
(assert (distinct p20 p33))
(assert (distinct p6 p30))
(assert (distinct p28 p33))
(assert (distinct p31 p48))
(assert (distinct p35 p51))
(assert (distinct p7 p53))
(assert (distinct p32 p53))
(assert (distinct p36 p50))
(assert (distinct p19 p44))
(assert (distinct p39 p47))
(assert (distinct p44 p50))
(assert (distinct p2 p19))
(assert (distinct p16 p45))
(assert (distinct p20 p42))
(assert (distinct p3 p52))
(assert (distinct p23 p55))
(assert (distinct p6 p7))
(assert (distinct p4 p49))
(assert (distinct p24 p46))
(assert (distinct p7 p48))
(assert (distinct p11 p35))
(assert (distinct p36 p55))
(assert (distinct p19 p35))
(assert (distinct p44 p55))
(assert (distinct p9 p21))
(assert (distinct p16 p54))
(assert (distinct p20 p47))
(assert (distinct p3 p11))
(assert (distinct p25 p36))
(assert (distinct p6 p16))
(assert (distinct p48 p52))
(assert (distinct p24 p43))
(assert (distinct p7 p39))
(assert (distinct p11 p46))
(assert (distinct p19 p30))
(assert (distinct p41 p51))
(assert (distinct p9 p28))
(assert (distinct p15 p18))
(assert (distinct p13 p32))
(assert (distinct p16 p51))
(assert (distinct p20 p56))
(assert (distinct p25 p43))
(assert (distinct p6 p9))
(assert (distinct p28 p56))
(assert (distinct p53 p54))
(assert (distinct p21 p31))
(assert (distinct p24 p36))
(assert (distinct p7 p26))
(assert (distinct p29 p47))
(assert (distinct p33 p42))
(assert (distinct p32 p36))
(assert (distinct p15 p25))
(assert (distinct p40 p49))
(assert (distinct p13 p23))
(assert (distinct p3 p29))
(assert (distinct p25 p50))
(assert (distinct p1 p43))
(assert (distinct p21 p38))
(assert (distinct p4 p40))
(assert (distinct p7 p17))
(assert (distinct p29 p38))
(assert (distinct p32 p41))
(assert (distinct p36 p46))
(assert (distinct p9 p10))
(assert (distinct p8 p52))
(assert (distinct p12 p53))
(assert (distinct p37 p53))
(assert (distinct p40 p42))
(assert (distinct p45 p53))
(assert (distinct p13 p14))
(assert (distinct p3 p24))
(assert (distinct p1 p34))
(assert (distinct p21 p45))
(assert (distinct p4 p45))
(assert (distinct p24 p50))
(assert (distinct p7 p12))
(assert (distinct p5 p54))
(assert (distinct p9 p49))
(assert (distinct p8 p41))
(assert (distinct p12 p46))
(assert (distinct p17 p49))
(assert (distinct p37 p52))
(assert (distinct p45 p52))
(assert (distinct p10 p24))
(assert (distinct p21 p44))
(assert (distinct p4 p22))
(assert (distinct p26 p33))
(assert (distinct p9 p56))
(assert (distinct p8 p34))
(assert (distinct p12 p35))
(assert (distinct p17 p56))
(assert (distinct p42 p50))
(assert (distinct p10 p25))
(assert (distinct p16 p23))
(assert (distinct p14 p29))
(assert (distinct p21 p51))
(assert (distinct p4 p27))
(assert (distinct p26 p42))
(assert (distinct p29 p51))
(assert (distinct p33 p54))
(assert (distinct p54 p55))
(assert (distinct p22 p30))
(assert (distinct p8 p31))
(assert (distinct p30 p46))
(assert (distinct p34 p43))
(assert (distinct p17 p47))
(assert (distinct p16 p32))
(assert (distinct p14 p22))
(assert (distinct p1 p55))
(assert (distinct p26 p51))
(assert (distinct p2 p42))
(assert (distinct p22 p39))
(assert (distinct p5 p35))
(assert (distinct p9 p38))
(assert (distinct p8 p24))
(assert (distinct p30 p39))
(assert (distinct p34 p36))
(assert (distinct p17 p38))
(assert (distinct p37 p41))
(assert (distinct p10 p11))
(assert (distinct p13 p50))
(assert (distinct p38 p56))
(assert (distinct p46 p56))
(assert (distinct p14 p15))
(assert (distinct p1 p14))
(assert (distinct p4 p9))
(assert (distinct p2 p35))
(assert (distinct p22 p48))
(assert (distinct p5 p42))
(assert (distinct p9 p45))
(assert (distinct p8 p13))
(assert (distinct p17 p29))
(assert (distinct p6 p55))
(assert (distinct p10 p52))
(assert (distinct p13 p41))
(assert (distinct p18 p52))
(assert (distinct p38 p49))
(assert (distinct p25 p28))
(assert (distinct p46 p49))
(assert (distinct p11 p19))
(assert (distinct p22 p41))
(assert (distinct p5 p17))
(assert (distinct p27 p38))
(assert (distinct p17 p20))
(assert (distinct p23 p26))
(assert (distinct p10 p53))
(assert (distinct p13 p40))
(assert (distinct p18 p53))
(assert (distinct p43 p53))
(assert (distinct p11 p30))
(assert (distinct p1 p28))
(assert (distinct p15 p34))
(assert (distinct p22 p50))
(assert (distinct p5 p32))
(assert (distinct p27 p45))
(assert (distinct p30 p50))
(assert (distinct p34 p55))
(assert (distinct p31 p49))
(assert (distinct p35 p48))
(assert (distinct p18 p46))
(assert (distinct p1 p19))
(assert (distinct p15 p41))
(assert (distinct p2 p54))
(assert (distinct p5 p7))
(assert (distinct p27 p56))
(assert (distinct p47 p51))
(assert (distinct p3 p45))
(assert (distinct p23 p44))
(assert (distinct p6 p34))
(assert (distinct p10 p39))
(assert (distinct p18 p39))
(assert (distinct p38 p44))
(assert (distinct p14 p51))
(assert (distinct p15 p52))
(assert (distinct p2 p15))
(assert (distinct p5 p14))
(assert (distinct p47 p54))
(assert (distinct p3 p40))
(assert (distinct p23 p35))
(assert (distinct p6 p43))
(assert (distinct p10 p48))
(assert (distinct p31 p35))
(assert (distinct p18 p32))
(assert (distinct p11 p55))
(assert (distinct p14 p44))
(assert (distinct p19 p55))
(assert (distinct p12 p30))
(assert (distinct p20 p27))
(assert (distinct p23 p38))
(assert (distinct p6 p20))
(assert (distinct p28 p43))
(assert (distinct p31 p38))
(assert (distinct p24 p31))
(assert (distinct p7 p51))
(assert (distinct p11 p50))
(assert (distinct p14 p37))
(assert (distinct p19 p50))
(assert (distinct p39 p53))
(assert (distinct p12 p19))
(assert (distinct p2 p25))
(assert (distinct p16 p39))
(assert (distinct p20 p36))
(assert (distinct p6 p29))
(assert (distinct p28 p36))
(assert (distinct p31 p45))
(assert (distinct p35 p52))
(assert (distinct p7 p54))
(assert (distinct p32 p56))
(assert (distinct p36 p49))
(assert (distinct p19 p41))
(assert (distinct p39 p48))
(assert (distinct p44 p49))
(assert (distinct p2 p18))
(assert (distinct p16 p48))
(assert (distinct p20 p41))
(assert (distinct p3 p49))
(assert (distinct p23 p56))
(assert (distinct p48 p54))
(assert (distinct p4 p52))
(assert (distinct p24 p45))
(assert (distinct p7 p45))
(assert (distinct p11 p36))
(assert (distinct p19 p36))
(assert (distinct p9 p22))
(assert (distinct p16 p53))
(assert (distinct p20 p50))
(assert (distinct p3 p12))
(assert (distinct p25 p37))
(assert (distinct p6 p15))
(assert (distinct p28 p50))
(assert (distinct p48 p51))
(assert (distinct p24 p38))
(assert (distinct p7 p40))
(assert (distinct p11 p43))
(assert (distinct p32 p38))
(assert (distinct p19 p27))
(assert (distinct p41 p52))
(assert (distinct p9 p29))
(assert (distinct p15 p23))
(assert (distinct p13 p25))
(assert (distinct p20 p55))
(assert (distinct p25 p44))
(assert (distinct p28 p55))
(assert (distinct p53 p55))
(assert (distinct p21 p32))
(assert (distinct p4 p34))
(assert (distinct p24 p35))
(assert (distinct p7 p31))
(assert (distinct p29 p48))
(assert (distinct p33 p43))
(assert (distinct p32 p35))
(assert (distinct p8 p54))
(assert (distinct p15 p26))
(assert (distinct p40 p52))
(assert (distinct p13 p24))
(assert (distinct p3 p30))
(assert (distinct p25 p51))
(assert (distinct p1 p44))
(assert (distinct p21 p39))
(assert (distinct p4 p39))
(assert (distinct p7 p18))
(assert (distinct p29 p39))
(assert (distinct p33 p34))
(assert (distinct p32 p44))
(assert (distinct p36 p45))
(assert (distinct p9 p11))
(assert (distinct p8 p51))
(assert (distinct p12 p56))
(assert (distinct p37 p54))
(assert (distinct p40 p41))
(assert (distinct p45 p54))
(assert (distinct p13 p15))
(assert (distinct p3 p21))
(assert (distinct p1 p35))
(assert (distinct p21 p46))
(assert (distinct p4 p48))
(assert (distinct p24 p49))
(assert (distinct p7 p9))
(assert (distinct p5 p55))
(assert (distinct p9 p50))
(assert (distinct p8 p44))
(assert (distinct p12 p45))
(assert (distinct p17 p50))
(assert (distinct p10 p23))
(assert (distinct p21 p53))
(assert (distinct p4 p21))
(assert (distinct p26 p40))
(assert (distinct p29 p53))
(assert (distinct p8 p33))
(assert (distinct p12 p38))
(assert (distinct p17 p41))
(assert (distinct p42 p49))
(assert (distinct p10 p32))
(assert (distinct p16 p18))
(assert (distinct p14 p28))
(assert (distinct p1 p49))
(assert (distinct p21 p52))
(assert (distinct p4 p30))
(assert (distinct p26 p41))
(assert (distinct p29 p52))
(check-sat)
(exit)