repositories
/
mc1516the.git
/ blob
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
history
|
raw
|
HEAD
Merge branch 'master' of gitlab.science.ru.nl:mlubbers/mc1516the
[mc1516the.git]
/
uppaal
/
2intermediateTrace.xtr
1
1
2
1
3
1
4
1
5
1
6
1
7
1
8
5
9
1
10
1
11
1
12
1
13
1
14
2
15
.
16
.
17
0
18
0
19
0
20
0
21
0
22
0
23
0
24
0
25
0
26
0
27
0
28
0
29
0
30
0
31
0
32
0
33
0
34
0
35
0
36
0
37
0
38
0
39
0
40
0
41
0
42
0
43
0
44
0
45
0
46
0
47
0
48
0
49
0
50
0
51
0
52
0
53
2
54
0
55
2
56
2
57
2
58
4
59
2
60
3
61
3
62
2
63
2
64
3
65
2
66
3
67
2
68
3
69
0
70
2
71
1
72
2
73
0
74
2
75
4
76
2
77
4
78
0
79
0
80
.
81
0
82
1
83
1
84
1
85
1
86
1
87
1
88
5
89
1
90
1
91
1
92
1
93
1
94
2
95
.
96
.
97
0
98
0
99
0
100
0
101
0
102
1
103
0
104
0
105
0
106
0
107
0
108
1
109
0
110
0
111
0
112
0
113
0
114
0
115
0
116
0
117
0
118
0
119
0
120
0
121
0
122
0
123
0
124
0
125
0
126
0
127
0
128
0
129
0
130
0
131
0
132
0
133
2
134
0
135
2
136
2
137
2
138
4
139
2
140
3
141
3
142
2
143
2
144
3
145
2
146
3
147
2
148
3
149
0
150
2
151
1
152
2
153
0
154
2
155
4
156
2
157
4
158
1
159
0
160
.
161
0 1 ;
162
13 2 ;
163
.
164
0
165
0
166
1
167
1
168
1
169
1
170
1
171
5
172
1
173
1
174
1
175
1
176
1
177
2
178
.
179
.
180
0
181
0
182
0
183
0
184
0
185
1
186
0
187
0
188
0
189
0
190
0
191
1
192
0
193
0
194
0
195
0
196
0
197
1
198
0
199
0
200
0
201
0
202
0
203
1
204
0
205
0
206
0
207
0
208
0
209
0
210
0
211
0
212
0
213
0
214
0
215
0
216
2
217
0
218
2
219
2
220
2
221
4
222
2
223
3
224
3
225
2
226
2
227
3
228
2
229
3
230
2
231
3
232
0
233
2
234
1
235
2
236
0
237
2
238
4
239
2
240
4
241
2
242
0
243
.
244
1 1 ;
245
13 2 ;
246
.
247
0
248
0
249
0
250
1
251
1
252
1
253
1
254
5
255
1
256
1
257
1
258
1
259
1
260
2
261
.
262
.
263
0
264
0
265
0
266
0
267
0
268
1
269
0
270
0
271
0
272
0
273
0
274
1
275
0
276
0
277
0
278
0
279
0
280
1
281
0
282
0
283
0
284
0
285
0
286
1
287
0
288
0
289
0
290
0
291
1
292
1
293
0
294
0
295
0
296
0
297
0
298
0
299
2
300
0
301
2
302
2
303
2
304
4
305
2
306
3
307
3
308
2
309
2
310
3
311
2
312
3
313
2
314
3
315
0
316
2
317
1
318
2
319
0
320
2
321
4
322
2
323
4
324
3
325
0
326
.
327
2 1 ;
328
13 2 ;
329
.
330
0
331
0
332
0
333
0
334
1
335
1
336
1
337
5
338
1
339
1
340
1
341
1
342
1
343
2
344
.
345
.
346
0
347
0
348
0
349
0
350
0
351
1
352
0
353
0
354
0
355
0
356
0
357
1
358
0
359
0
360
0
361
1
362
1
363
1
364
0
365
0
366
0
367
0
368
0
369
1
370
0
371
0
372
0
373
0
374
1
375
1
376
0
377
0
378
0
379
0
380
0
381
0
382
2
383
0
384
2
385
2
386
2
387
4
388
2
389
3
390
3
391
2
392
2
393
3
394
2
395
3
396
2
397
3
398
0
399
2
400
1
401
2
402
0
403
2
404
4
405
2
406
4
407
4
408
0
409
.
410
3 1 ;
411
13 2 ;
412
.
413
0
414
0
415
0
416
0
417
0
418
1
419
1
420
5
421
1
422
1
423
1
424
1
425
1
426
2
427
.
428
.
429
0
430
0
431
0
432
0
433
0
434
1
435
0
436
0
437
0
438
0
439
0
440
1
441
0
442
0
443
0
444
1
445
1
446
1
447
0
448
0
449
0
450
0
451
0
452
1
453
0
454
0
455
0
456
0
457
1
458
1
459
0
460
0
461
1
462
1
463
1
464
0
465
2
466
0
467
2
468
2
469
2
470
4
471
2
472
3
473
3
474
2
475
2
476
3
477
2
478
3
479
2
480
3
481
0
482
2
483
1
484
2
485
0
486
2
487
4
488
2
489
4
490
5
491
0
492
.
493
4 1 ;
494
13 2 ;
495
.
496
0
497
0
498
0
499
0
500
0
501
0
502
1
503
5
504
1
505
1
506
1
507
1
508
1
509
2
510
.
511
.
512
0
513
0
514
0
515
0
516
0
517
1
518
0
519
0
520
0
521
1
522
1
523
1
524
0
525
0
526
0
527
1
528
1
529
1
530
0
531
0
532
0
533
0
534
0
535
1
536
0
537
0
538
0
539
0
540
1
541
1
542
0
543
0
544
1
545
1
546
1
547
0
548
2
549
0
550
2
551
2
552
2
553
4
554
2
555
3
556
3
557
2
558
2
559
3
560
2
561
3
562
2
563
3
564
0
565
2
566
1
567
2
568
0
569
2
570
4
571
2
572
4
573
6
574
0
575
.
576
5 1 ;
577
13 2 ;
578
.
579
0
580
0
581
0
582
0
583
0
584
0
585
0
586
5
587
1
588
1
589
1
590
1
591
1
592
2
593
.
594
.
595
0
596
0
597
0
598
0
599
0
600
1
601
0
602
0
603
0
604
1
605
1
606
1
607
0
608
0
609
0
610
1
611
1
612
1
613
0
614
0
615
0
616
0
617
1
618
1
619
0
620
0
621
0
622
0
623
1
624
1
625
0
626
0
627
1
628
1
629
1
630
0
631
2
632
0
633
2
634
2
635
2
636
4
637
2
638
3
639
3
640
2
641
2
642
3
643
2
644
3
645
2
646
3
647
0
648
2
649
1
650
2
651
0
652
2
653
4
654
2
655
4
656
7
657
0
658
.
659
6 1 ;
660
13 2 ;
661
.
662
0
663
0
664
0
665
0
666
0
667
0
668
0
669
4
670
1
671
1
672
1
673
1
674
1
675
2
676
.
677
.
678
0
679
0
680
0
681
0
682
0
683
1
684
0
685
0
686
0
687
1
688
1
689
1
690
0
691
0
692
0
693
1
694
1
695
1
696
0
697
0
698
0
699
1
700
1
701
1
702
0
703
0
704
0
705
0
706
1
707
1
708
0
709
0
710
1
711
1
712
1
713
0
714
2
715
0
716
2
717
2
718
2
719
4
720
2
721
3
722
3
723
2
724
2
725
3
726
2
727
3
728
2
729
3
730
0
731
2
732
1
733
2
734
0
735
2
736
4
737
2
738
4
739
8
740
0
741
.
742
7 9 ;
743
13 2 ;
744
.
745
0
746
0
747
0
748
0
749
0
750
0
751
0
752
4
753
0
754
1
755
1
756
1
757
1
758
2
759
.
760
.
761
1
762
1
763
1
764
0
765
0
766
1
767
0
768
0
769
0
770
1
771
1
772
1
773
0
774
0
775
0
776
1
777
1
778
1
779
0
780
0
781
0
782
1
783
1
784
1
785
0
786
0
787
0
788
0
789
1
790
1
791
0
792
0
793
1
794
1
795
1
796
0
797
2
798
0
799
2
800
2
801
2
802
4
803
2
804
3
805
3
806
2
807
2
808
3
809
2
810
3
811
2
812
3
813
0
814
2
815
1
816
2
817
0
818
2
819
4
820
2
821
4
822
9
823
0
824
.
825
8 1 ;
826
13 2 ;
827
.
828
0
829
0
830
0
831
0
832
0
833
0
834
0
835
4
836
0
837
0
838
1
839
1
840
1
841
2
842
.
843
.
844
1
845
1
846
1
847
0
848
0
849
1
850
1
851
0
852
0
853
1
854
1
855
1
856
1
857
0
858
0
859
1
860
1
861
1
862
0
863
0
864
0
865
1
866
1
867
1
868
0
869
0
870
0
871
0
872
1
873
1
874
0
875
0
876
1
877
1
878
1
879
0
880
2
881
0
882
2
883
2
884
2
885
4
886
2
887
3
888
3
889
2
890
2
891
3
892
2
893
3
894
2
895
3
896
0
897
2
898
1
899
2
900
0
901
2
902
4
903
2
904
4
905
10
906
0
907
.
908
9 1 ;
909
13 2 ;
910
.
911
0
912
0
913
0
914
0
915
0
916
0
917
0
918
4
919
0
920
0
921
0
922
1
923
1
924
2
925
.
926
.
927
1
928
1
929
1
930
0
931
0
932
1
933
1
934
0
935
0
936
1
937
1
938
1
939
1
940
0
941
0
942
1
943
1
944
1
945
1
946
1
947
0
948
1
949
1
950
1
951
0
952
0
953
0
954
0
955
1
956
1
957
0
958
0
959
1
960
1
961
1
962
0
963
2
964
0
965
2
966
2
967
2
968
4
969
2
970
3
971
3
972
2
973
2
974
3
975
2
976
3
977
2
978
3
979
0
980
2
981
1
982
2
983
0
984
2
985
4
986
2
987
4
988
11
989
0
990
.
991
10 1 ;
992
13 2 ;
993
.
994
0
995
0
996
0
997
0
998
0
999
0
1000
0
1001
4
1002
0
1003
0
1004
0
1005
0
1006
1
1007
2
1008
.
1009
.
1010
1
1011
1
1012
1
1013
0
1014
0
1015
1
1016
1
1017
0
1018
0
1019
1
1020
1
1021
1
1022
1
1023
0
1024
0
1025
1
1026
1
1027
1
1028
1
1029
1
1030
0
1031
1
1032
1
1033
1
1034
0
1035
1
1036
0
1037
0
1038
1
1039
1
1040
0
1041
1
1042
1
1043
1
1044
1
1045
0
1046
2
1047
0
1048
2
1049
2
1050
2
1051
4
1052
2
1053
3
1054
3
1055
2
1056
2
1057
3
1058
2
1059
3
1060
2
1061
3
1062
0
1063
2
1064
1
1065
2
1066
0
1067
2
1068
4
1069
2
1070
4
1071
12
1072
0
1073
.
1074
11 1 ;
1075
13 2 ;
1076
.
1077
0
1078
0
1079
0
1080
0
1081
0
1082
0
1083
0
1084
4
1085
0
1086
0
1087
0
1088
0
1089
0
1090
2
1091
.
1092
.
1093
1
1094
1
1095
1
1096
0
1097
0
1098
1
1099
1
1100
0
1101
0
1102
1
1103
1
1104
1
1105
1
1106
0
1107
0
1108
1
1109
1
1110
1
1111
1
1112
1
1113
0
1114
1
1115
1
1116
1
1117
1
1118
1
1119
0
1120
0
1121
1
1122
1
1123
1
1124
1
1125
1
1126
1
1127
1
1128
0
1129
2
1130
0
1131
2
1132
2
1133
2
1134
4
1135
2
1136
3
1137
3
1138
2
1139
2
1140
3
1141
2
1142
3
1143
2
1144
3
1145
0
1146
2
1147
1
1148
2
1149
0
1150
2
1151
4
1152
2
1153
4
1154
13
1155
0
1156
.
1157
12 1 ;
1158
13 2 ;
1159
.
1160
2
1161
2
1162
2
1163
2
1164
2
1165
2
1166
2
1167
3
1168
2
1169
2
1170
2
1171
2
1172
2
1173
1
1174
.
1175
.
1176
1
1177
1
1178
1
1179
0
1180
0
1181
1
1182
1
1183
0
1184
0
1185
1
1186
1
1187
1
1188
1
1189
0
1190
0
1191
1
1192
1
1193
1
1194
1
1195
1
1196
0
1197
1
1198
1
1199
1
1200
1
1201
1
1202
0
1203
0
1204
1
1205
1
1206
1
1207
1
1208
1
1209
1
1210
1
1211
0
1212
2
1213
0
1214
2
1215
2
1216
2
1217
4
1218
2
1219
3
1220
3
1221
2
1222
2
1223
3
1224
2
1225
3
1226
2
1227
3
1228
0
1229
2
1230
1
1231
2
1232
0
1233
2
1234
4
1235
2
1236
4
1237
13
1238
0
1239
.
1240
13 1 ;
1241
0 0 ;
1242
1 0 ;
1243
2 0 ;
1244
3 0 ;
1245
4 0 ;
1246
5 0 ;
1247
6 0 ;
1248
7 8 ;
1249
8 0 ;
1250
9 0 ;
1251
10 0 ;
1252
11 0 ;
1253
12 0 ;
1254
.
1255
2
1256
2
1257
2
1258
2
1259
2
1260
2
1261
2
1262
0
1263
2
1264
2
1265
2
1266
2
1267
2
1268
1
1269
.
1270
.
1271
1
1272
1
1273
1
1274
0
1275
0
1276
1
1277
1
1278
0
1279
0
1280
1
1281
1
1282
1
1283
1
1284
0
1285
0
1286
1
1287
1
1288
1
1289
1
1290
1
1291
0
1292
1
1293
1
1294
1
1295
1
1296
1
1297
0
1298
0
1299
1
1300
1
1301
1
1302
1
1303
1
1304
1
1305
1
1306
0
1307
2
1308
0
1309
2
1310
2
1311
2
1312
4
1313
2
1314
3
1315
3
1316
2
1317
2
1318
3
1319
2
1320
3
1321
2
1322
3
1323
0
1324
2
1325
1
1326
2
1327
0
1328
2
1329
4
1330
2
1331
4
1332
13
1333
0
1334
.
1335
7 4 ;
1336
7 6 ;
1337
.
1338
2
1339
2
1340
2
1341
2
1342
2
1343
2
1344
2
1345
0
1346
2
1347
2
1348
2
1349
2
1350
2
1351
1
1352
.
1353
.
1354
1
1355
1
1356
1
1357
0
1358
0
1359
1
1360
1
1361
0
1362
0
1363
1
1364
1
1365
1
1366
1
1367
0
1368
0
1369
1
1370
1
1371
1
1372
0
1373
1
1374
1
1375
1
1376
1
1377
1
1378
1
1379
1
1380
0
1381
0
1382
1
1383
1
1384
1
1385
1
1386
1
1387
1
1388
1
1389
0
1390
2
1391
0
1392
2
1393
2
1394
2
1395
4
1396
2
1397
3
1398
3
1399
2
1400
2
1401
3
1402
2
1403
3
1404
2
1405
3
1406
0
1407
2
1408
1
1409
2
1410
1
1411
2
1412
4
1413
2
1414
4
1415
13
1416
0
1417
.
1418
10 3 ;
1419
.
1420
2
1421
2
1422
2
1423
2
1424
2
1425
2
1426
2
1427
0
1428
2
1429
2
1430
2
1431
2
1432
2
1433
1
1434
.
1435
.
1436
1
1437
1
1438
1
1439
0
1440
0
1441
1
1442
1
1443
0
1444
0
1445
1
1446
1
1447
1
1448
1
1449
0
1450
0
1451
1
1452
1
1453
1
1454
0
1455
1
1456
1
1457
1
1458
1
1459
1
1460
1
1461
1
1462
0
1463
1
1464
1
1465
0
1466
1
1467
1
1468
1
1469
1
1470
1
1471
0
1472
2
1473
0
1474
2
1475
2
1476
2
1477
3
1478
2
1479
3
1480
3
1481
2
1482
2
1483
3
1484
2
1485
3
1486
2
1487
3
1488
0
1489
2
1490
1
1491
2
1492
1
1493
2
1494
4
1495
2
1496
4
1497
13
1498
0
1499
.
1500
2 2 ;
1501
.
1502
2
1503
2
1504
2
1505
2
1506
2
1507
2
1508
2
1509
0
1510
2
1511
2
1512
2
1513
2
1514
2
1515
1
1516
.
1517
.
1518
1
1519
1
1520
1
1521
0
1522
0
1523
1
1524
1
1525
0
1526
0
1527
1
1528
1
1529
1
1530
1
1531
0
1532
0
1533
1
1534
1
1535
1
1536
0
1537
1
1538
1
1539
1
1540
1
1541
1
1542
1
1543
1
1544
1
1545
1
1546
0
1547
0
1548
1
1549
1
1550
1
1551
1
1552
1
1553
0
1554
2
1555
0
1556
2
1557
2
1558
2
1559
2
1560
2
1561
3
1562
3
1563
2
1564
2
1565
3
1566
2
1567
3
1568
2
1569
3
1570
0
1571
2
1572
1
1573
2
1574
1
1575
2
1576
4
1577
2
1578
4
1579
13
1580
0
1581
.
1582
2 2 ;
1583
.
1584
2
1585
2
1586
2
1587
2
1588
2
1589
2
1590
2
1591
0
1592
2
1593
2
1594
2
1595
2
1596
2
1597
1
1598
.
1599
.
1600
1
1601
1
1602
1
1603
0
1604
0
1605
1
1606
1
1607
0
1608
1
1609
1
1610
0
1611
1
1612
1
1613
0
1614
0
1615
1
1616
1
1617
1
1618
0
1619
1
1620
1
1621
1
1622
1
1623
1
1624
1
1625
1
1626
1
1627
1
1628
0
1629
0
1630
1
1631
1
1632
1
1633
1
1634
1
1635
0
1636
2
1637
0
1638
2
1639
2
1640
2
1641
2
1642
2
1643
3
1644
3
1645
2
1646
2
1647
2
1648
2
1649
3
1650
2
1651
3
1652
0
1653
2
1654
1
1655
2
1656
1
1657
2
1658
4
1659
2
1660
4
1661
13
1662
0
1663
.
1664
5 2 ;
1665
.
1666
2
1667
2
1668
2
1669
2
1670
2
1671
2
1672
2
1673
0
1674
2
1675
2
1676
2
1677
2
1678
2
1679
1
1680
.
1681
.
1682
1
1683
1
1684
1
1685
0
1686
0
1687
1
1688
1
1689
1
1690
1
1691
0
1692
0
1693
1
1694
1
1695
0
1696
0
1697
1
1698
1
1699
1
1700
0
1701
1
1702
1
1703
1
1704
1
1705
1
1706
1
1707
1
1708
1
1709
1
1710
0
1711
0
1712
1
1713
1
1714
1
1715
1
1716
1
1717
0
1718
2
1719
0
1720
2
1721
2
1722
2
1723
2
1724
2
1725
3
1726
3
1727
2
1728
2
1729
1
1730
2
1731
3
1732
2
1733
3
1734
0
1735
2
1736
1
1737
2
1738
1
1739
2
1740
4
1741
2
1742
4
1743
13
1744
0
1745
.
1746
5 2 ;
1747
.
1748
2
1749
2
1750
2
1751
2
1752
2
1753
2
1754
2
1755
0
1756
2
1757
2
1758
2
1759
2
1760
2
1761
1
1762
.
1763
.
1764
1
1765
1
1766
1
1767
0
1768
0
1769
1
1770
1
1771
1
1772
1
1773
0
1774
0
1775
1
1776
1
1777
0
1778
0
1779
1
1780
1
1781
1
1782
1
1783
1
1784
1
1785
1
1786
1
1787
1
1788
1
1789
1
1790
1
1791
1
1792
0
1793
0
1794
0
1795
1
1796
1
1797
1
1798
1
1799
0
1800
2
1801
0
1802
2
1803
2
1804
2
1805
2
1806
2
1807
3
1808
3
1809
2
1810
2
1811
1
1812
2
1813
3
1814
2
1815
3
1816
0
1817
2
1818
1
1819
2
1820
1
1821
2
1822
4
1823
2
1824
3
1825
13
1826
0
1827
.
1828
12 2 ;
1829
.
1830
2
1831
2
1832
2
1833
2
1834
2
1835
2
1836
2
1837
0
1838
2
1839
2
1840
2
1841
2
1842
2
1843
1
1844
.
1845
.
1846
1
1847
1
1848
1
1849
0
1850
0
1851
1
1852
1
1853
1
1854
1
1855
0
1856
0
1857
1
1858
1
1859
0
1860
0
1861
1
1862
1
1863
0
1864
1
1865
1
1866
1
1867
1
1868
1
1869
1
1870
1
1871
1
1872
1
1873
1
1874
0
1875
1
1876
0
1877
1
1878
1
1879
1
1880
1
1881
0
1882
2
1883
0
1884
2
1885
3
1886
2
1887
2
1888
2
1889
3
1890
3
1891
2
1892
2
1893
1
1894
2
1895
3
1896
2
1897
3
1898
0
1899
2
1900
1
1901
2
1902
1
1903
2
1904
4
1905
2
1906
3
1907
13
1908
0
1909
.
1910
1 3 ;
1911
.
1912
2
1913
2
1914
2
1915
2
1916
2
1917
2
1918
2
1919
0
1920
2
1921
2
1922
2
1923
2
1924
2
1925
1
1926
.
1927
.
1928
1
1929
1
1930
1
1931
0
1932
0
1933
1
1934
1
1935
1
1936
1
1937
0
1938
0
1939
1
1940
1
1941
0
1942
0
1943
1
1944
1
1945
0
1946
1
1947
1
1948
1
1949
1
1950
1
1951
0
1952
1
1953
1
1954
1
1955
1
1956
0
1957
1
1958
0
1959
1
1960
1
1961
1
1962
1
1963
1
1964
2
1965
0
1966
2
1967
4
1968
2
1969
2
1970
2
1971
3
1972
3
1973
2
1974
2
1975
1
1976
2
1977
3
1978
2
1979
3
1980
0
1981
2
1982
1
1983
2
1984
1
1985
2
1986
4
1987
2
1988
3
1989
13
1990
0
1991
.
1992
1 3 ;
1993
.
1994
2
1995
2
1996
2
1997
2
1998
2
1999
2
2000
2
2001
3
2002
2
2003
2
2004
2
2005
2
2006
2
2007
1
2008
.
2009
.
2010
1
2011
1
2012
1
2013
0
2014
0
2015
1
2016
1
2017
1
2018
1
2019
1
2020
0
2021
1
2022
1
2023
0
2024
0
2025
1
2026
1
2027
0
2028
1
2029
1
2030
1
2031
0
2032
1
2033
0
2034
1
2035
1
2036
1
2037
1
2038
0
2039
1
2040
0
2041
1
2042
1
2043
1
2044
1
2045
1
2046
2
2047
0
2048
2
2049
4
2050
2
2051
2
2052
2
2053
3
2054
3
2055
2
2056
2
2057
1
2058
2
2059
3
2060
1
2061
3
2062
0
2063
2
2064
1
2065
2
2066
1
2067
2
2068
4
2069
2
2070
3
2071
13
2072
0
2073
.
2074
7 3 ;
2075
.
2076
2
2077
2
2078
2
2079
2
2080
2
2081
2
2082
2
2083
1
2084
2
2085
2
2086
2
2087
2
2088
2
2089
1
2090
.
2091
.
2092
1
2093
1
2094
1
2095
0
2096
0
2097
1
2098
1
2099
1
2100
1
2101
1
2102
0
2103
1
2104
1
2105
0
2106
0
2107
1
2108
1
2109
0
2110
1
2111
1
2112
1
2113
0
2114
1
2115
0
2116
1
2117
1
2118
1
2119
1
2120
0
2121
1
2122
0
2123
1
2124
1
2125
1
2126
1
2127
1
2128
2
2129
0
2130
2
2131
4
2132
2
2133
2
2134
2
2135
3
2136
3
2137
2
2138
2
2139
1
2140
2
2141
3
2142
1
2143
3
2144
0
2145
2
2146
1
2147
2
2148
1
2149
2
2150
4
2151
2
2152
3
2153
13
2154
0
2155
.
2156
7 5 ;
2157
7 6 ;
2158
.
2159
2
2160
2
2161
2
2162
2
2163
2
2164
2
2165
2
2166
1
2167
2
2168
2
2169
2
2170
2
2171
2
2172
1
2173
.
2174
.
2175
1
2176
1
2177
1
2178
0
2179
0
2180
1
2181
1
2182
1
2183
1
2184
1
2185
0
2186
1
2187
1
2188
0
2189
0
2190
1
2191
1
2192
0
2193
1
2194
0
2195
1
2196
1
2197
1
2198
0
2199
1
2200
1
2201
1
2202
1
2203
0
2204
1
2205
0
2206
1
2207
1
2208
1
2209
1
2210
1
2211
2
2212
0
2213
2
2214
4
2215
2
2216
2
2217
2
2218
3
2219
3
2220
2
2221
2
2222
1
2223
2
2224
3
2225
1
2226
3
2227
0
2228
2
2229
1
2230
2
2231
2
2232
2
2233
4
2234
2
2235
3
2236
13
2237
0
2238
.
2239
10 3 ;
2240
.
2241
2
2242
2
2243
2
2244
2
2245
2
2246
2
2247
2
2248
1
2249
2
2250
2
2251
2
2252
2
2253
2
2254
1
2255
.
2256
.
2257
1
2258
1
2259
1
2260
0
2261
0
2262
1
2263
1
2264
1
2265
1
2266
1
2267
0
2268
1
2269
1
2270
0
2271
0
2272
1
2273
1
2274
0
2275
1
2276
1
2277
1
2278
1
2279
1
2280
0
2281
1
2282
1
2283
1
2284
1
2285
0
2286
1
2287
0
2288
0
2289
1
2290
1
2291
1
2292
1
2293
2
2294
0
2295
2
2296
4
2297
2
2298
2
2299
2
2300
3
2301
3
2302
2
2303
2
2304
1
2305
2
2306
3
2307
1
2308
3
2309
0
2310
2
2311
1
2312
2
2313
2
2314
2
2315
3
2316
2
2317
3
2318
13
2319
0
2320
.
2321
11 2 ;
2322
.
2323
2
2324
2
2325
2
2326
2
2327
2
2328
2
2329
2
2330
1
2331
2
2332
2
2333
2
2334
2
2335
2
2336
1
2337
.
2338
.
2339
1
2340
1
2341
1
2342
0
2343
0
2344
1
2345
1
2346
1
2347
1
2348
1
2349
0
2350
1
2351
1
2352
0
2353
0
2354
1
2355
1
2356
0
2357
1
2358
1
2359
1
2360
1
2361
1
2362
0
2363
1
2364
1
2365
1
2366
1
2367
0
2368
1
2369
0
2370
1
2371
1
2372
1
2373
0
2374
1
2375
2
2376
0
2377
2
2378
4
2379
2
2380
2
2381
2
2382
3
2383
3
2384
1
2385
2
2386
1
2387
2
2388
3
2389
1
2390
3
2391
0
2392
2
2393
1
2394
2
2395
2
2396
2
2397
3
2398
2
2399
3
2400
13
2401
0
2402
.
2403
4 2 ;
2404
.
2405
2
2406
2
2407
2
2408
2
2409
2
2410
2
2411
2
2412
1
2413
2
2414
2
2415
2
2416
2
2417
2
2418
1
2419
.
2420
.
2421
1
2422
1
2423
1
2424
0
2425
0
2426
1
2427
1
2428
1
2429
1
2430
1
2431
0
2432
1
2433
1
2434
0
2435
0
2436
1
2437
1
2438
0
2439
1
2440
1
2441
1
2442
1
2443
1
2444
0
2445
1
2446
1
2447
1
2448
1
2449
0
2450
1
2451
1
2452
1
2453
1
2454
0
2455
0
2456
1
2457
2
2458
0
2459
2
2460
4
2461
2
2462
2
2463
2
2464
3
2465
3
2466
0
2467
2
2468
1
2469
2
2470
3
2471
1
2472
3
2473
0
2474
2
2475
1
2476
2
2477
2
2478
2
2479
3
2480
2
2481
3
2482
13
2483
0
2484
.
2485
4 2 ;
2486
.
2487
2
2488
2
2489
2
2490
2
2491
2
2492
2
2493
2
2494
1
2495
2
2496
2
2497
2
2498
2
2499
2
2500
1
2501
.
2502
.
2503
1
2504
1
2505
1
2506
0
2507
0
2508
1
2509
1
2510
1
2511
1
2512
1
2513
0
2514
1
2515
1
2516
1
2517
0
2518
1
2519
1
2520
0
2521
1
2522
1
2523
1
2524
1
2525
1
2526
0
2527
1
2528
0
2529
1
2530
1
2531
0
2532
1
2533
1
2534
1
2535
1
2536
0
2537
0
2538
1
2539
2
2540
0
2541
2
2542
4
2543
2
2544
2
2545
2
2546
3
2547
3
2548
0
2549
2
2550
1
2551
2
2552
3
2553
1
2554
3
2555
0
2556
2
2557
1
2558
2
2559
2
2560
2
2561
2
2562
2
2563
3
2564
13
2565
0
2566
.
2567
11 2 ;
2568
.
2569
2
2570
2
2571
2
2572
2
2573
2
2574
2
2575
2
2576
1
2577
2
2578
2
2579
2
2580
2
2581
2
2582
1
2583
.
2584
.
2585
1
2586
1
2587
1
2588
0
2589
0
2590
1
2591
1
2592
1
2593
1
2594
1
2595
0
2596
1
2597
1
2598
1
2599
0
2600
1
2601
1
2602
0
2603
1
2604
1
2605
1
2606
1
2607
1
2608
0
2609
1
2610
1
2611
1
2612
0
2613
0
2614
1
2615
1
2616
1
2617
1
2618
0
2619
0
2620
1
2621
2
2622
0
2623
2
2624
4
2625
2
2626
1
2627
2
2628
3
2629
3
2630
0
2631
2
2632
1
2633
2
2634
3
2635
1
2636
3
2637
0
2638
2
2639
1
2640
2
2641
2
2642
2
2643
2
2644
2
2645
3
2646
13
2647
0
2648
.
2649
2 2 ;
2650
.
2651
2
2652
2
2653
2
2654
2
2655
2
2656
2
2657
2
2658
1
2659
2
2660
2
2661
2
2662
2
2663
2
2664
1
2665
.
2666
.
2667
1
2668
1
2669
1
2670
0
2671
0
2672
1
2673
1
2674
1
2675
1
2676
1
2677
0
2678
1
2679
1
2680
1
2681
0
2682
1
2683
1
2684
0
2685
1
2686
1
2687
1
2688
1
2689
0
2690
0
2691
1
2692
1
2693
1
2694
0
2695
0
2696
1
2697
1
2698
1
2699
1
2700
0
2701
1
2702
1
2703
2
2704
0
2705
2
2706
4
2707
2
2708
1
2709
2
2710
3
2711
3
2712
0
2713
2
2714
1
2715
2
2716
4
2717
1
2718
3
2719
0
2720
2
2721
1
2722
2
2723
2
2724
2
2725
2
2726
2
2727
3
2728
13
2729
0
2730
.
2731
6 3 ;
2732
.
2733
2
2734
2
2735
2
2736
2
2737
2
2738
2
2739
2
2740
1
2741
2
2742
2
2743
2
2744
2
2745
2
2746
1
2747
.
2748
.
2749
1
2750
1
2751
1
2752
0
2753
0
2754
1
2755
1
2756
1
2757
1
2758
1
2759
0
2760
1
2761
1
2762
1
2763
0
2764
1
2765
1
2766
0
2767
1
2768
1
2769
0
2770
1
2771
1
2772
0
2773
1
2774
1
2775
1
2776
0
2777
0
2778
1
2779
1
2780
1
2781
1
2782
0
2783
1
2784
1
2785
2
2786
0
2787
2
2788
4
2789
2
2790
1
2791
2
2792
3
2793
3
2794
0
2795
2
2796
1
2797
2
2798
4
2799
1
2800
3
2801
0
2802
2
2803
1
2804
2
2805
3
2806
2
2807
2
2808
2
2809
3
2810
13
2811
0
2812
.
2813
10 3 ;
2814
.
2815
2
2816
2
2817
2
2818
2
2819
2
2820
2
2821
2
2822
1
2823
2
2824
2
2825
2
2826
2
2827
2
2828
1
2829
.
2830
.
2831
1
2832
1
2833
1
2834
0
2835
0
2836
1
2837
1
2838
1
2839
1
2840
1
2841
0
2842
1
2843
1
2844
1
2845
0
2846
1
2847
1
2848
0
2849
1
2850
1
2851
0
2852
0
2853
1
2854
1
2855
1
2856
1
2857
1
2858
0
2859
0
2860
1
2861
1
2862
1
2863
1
2864
0
2865
1
2866
1
2867
2
2868
0
2869
2
2870
4
2871
2
2872
1
2873
2
2874
3
2875
3
2876
0
2877
2
2878
1
2879
2
2880
4
2881
1
2882
3
2883
0
2884
2
2885
1
2886
2
2887
4
2888
2
2889
2
2890
2
2891
3
2892
13
2893
0
2894
.
2895
10 3 ;
2896
.
2897
2
2898
2
2899
2
2900
2
2901
2
2902
2
2903
2
2904
3
2905
2
2906
2
2907
2
2908
2
2909
2
2910
1
2911
.
2912
.
2913
1
2914
1
2915
1
2916
0
2917
0
2918
1
2919
1
2920
1
2921
1
2922
0
2923
0
2924
1
2925
1
2926
1
2927
0
2928
1
2929
1
2930
0
2931
1
2932
1
2933
0
2934
1
2935
1
2936
1
2937
1
2938
1
2939
1
2940
0
2941
0
2942
1
2943
1
2944
1
2945
1
2946
0
2947
1
2948
1
2949
2
2950
0
2951
2
2952
4
2953
2
2954
1
2955
2
2956
3
2957
3
2958
0
2959
2
2960
1
2961
2
2962
4
2963
2
2964
3
2965
0
2966
2
2967
1
2968
2
2969
4
2970
2
2971
2
2972
2
2973
3
2974
13
2975
0
2976
.
2977
7 2 ;
2978
.
2979
2
2980
2
2981
2
2982
2
2983
2
2984
2
2985
2
2986
1
2987
2
2988
2
2989
2
2990
2
2991
2
2992
1
2993
.
2994
.
2995
1
2996
1
2997
1
2998
0
2999
0
3000
1
3001
1
3002
1
3003
1
3004
0
3005
0
3006
1
3007
1
3008
1
3009
0
3010
1
3011
1
3012
0
3013
1
3014
1
3015
0
3016
1
3017
1
3018
1
3019
1
3020
1
3021
1
3022
0
3023
0
3024
1
3025
1
3026
1
3027
1
3028
0
3029
1
3030
1
3031
2
3032
0
3033
2
3034
4
3035
2
3036
1
3037
2
3038
3
3039
3
3040
0
3041
2
3042
1
3043
2
3044
4
3045
2
3046
3
3047
0
3048
2
3049
1
3050
2
3051
4
3052
2
3053
2
3054
2
3055
3
3056
13
3057
0
3058
.
3059
7 5 ;
3060
7 6 ;
3061
.
3062
2
3063
2
3064
2
3065
2
3066
2
3067
2
3068
2
3069
3
3070
2
3071
2
3072
2
3073
2
3074
2
3075
1
3076
.
3077
.
3078
1
3079
1
3080
1
3081
0
3082
0
3083
1
3084
1
3085
1
3086
1
3087
0
3088
0
3089
1
3090
1
3091
1
3092
0
3093
0
3094
1
3095
0
3096
1
3097
1
3098
0
3099
1
3100
1
3101
1
3102
1
3103
1
3104
1
3105
1
3106
0
3107
1
3108
1
3109
1
3110
1
3111
0
3112
1
3113
1
3114
2
3115
0
3116
2
3117
4
3118
2
3119
1
3120
2
3121
3
3122
3
3123
0
3124
2
3125
1
3126
2
3127
4
3128
3
3129
3
3130
0
3131
2
3132
1
3133
2
3134
4
3135
2
3136
2
3137
2
3138
3
3139
13
3140
0
3141
.
3142
7 2 ;
3143
.
3144
2
3145
2
3146
2
3147
2
3148
2
3149
2
3150
2
3151
1
3152
2
3153
2
3154
2
3155
2
3156
2
3157
1
3158
.
3159
.
3160
1
3161
1
3162
1
3163
0
3164
0
3165
1
3166
1
3167
1
3168
1
3169
0
3170
0
3171
1
3172
1
3173
1
3174
0
3175
0
3176
1
3177
0
3178
1
3179
1
3180
0
3181
1
3182
1
3183
1
3184
1
3185
1
3186
1
3187
1
3188
0
3189
1
3190
1
3191
1
3192
1
3193
0
3194
1
3195
1
3196
2
3197
0
3198
2
3199
4
3200
2
3201
1
3202
2
3203
3
3204
3
3205
0
3206
2
3207
1
3208
2
3209
4
3210
3
3211
3
3212
0
3213
2
3214
1
3215
2
3216
4
3217
2
3218
2
3219
2
3220
3
3221
13
3222
0
3223
.
3224
7 5 ;
3225
7 6 ;
3226
.
3227
2
3228
2
3229
2
3230
2
3231
2
3232
2
3233
2
3234
3
3235
2
3236
2
3237
2
3238
2
3239
2
3240
1
3241
.
3242
.
3243
1
3244
1
3245
1
3246
0
3247
0
3248
1
3249
1
3250
1
3251
1
3252
0
3253
0
3254
1
3255
1
3256
1
3257
0
3258
0
3259
1
3260
0
3261
1
3262
1
3263
0
3264
0
3265
1
3266
1
3267
1
3268
1
3269
1
3270
1
3271
0
3272
1
3273
1
3274
1
3275
1
3276
1
3277
1
3278
1
3279
2
3280
0
3281
2
3282
4
3283
2
3284
1
3285
2
3286
3
3287
3
3288
0
3289
2
3290
1
3291
2
3292
4
3293
4
3294
3
3295
0
3296
2
3297
1
3298
2
3299
4
3300
2
3301
2
3302
2
3303
3
3304
13
3305
0
3306
.
3307
7 2 ;
3308
.
3309
2
3310
2
3311
2
3312
2
3313
2
3314
2
3315
2
3316
2
3317
2
3318
2
3319
2
3320
2
3321
2
3322
0
3323
.
3324
.
3325
1
3326
1
3327
1
3328
0
3329
0
3330
1
3331
1
3332
1
3333
1
3334
0
3335
0
3336
1
3337
1
3338
1
3339
0
3340
0
3341
1
3342
0
3343
1
3344
1
3345
0
3346
0
3347
1
3348
1
3349
1
3350
1
3351
1
3352
1
3353
0
3354
1
3355
1
3356
1
3357
1
3358
1
3359
1
3360
1
3361
2
3362
0
3363
2
3364
4
3365
2
3366
1
3367
2
3368
3
3369
3
3370
0
3371
2
3372
1
3373
2
3374
4
3375
4
3376
3
3377
0
3378
2
3379
1
3380
2
3381
4
3382
2
3383
2
3384
2
3385
3
3386
13
3387
1
3388
.
3389
7 7 ;
3390
13 0 ;
3391
.
3392
.