Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3746)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

1.1 Bounds

• final states:

  {7}

• transitions:

  1405	→	53
  1405	→	1539
  1303	→	310
  1067	→	340
  223	→	53
  366	→	84
  1268	→	283
  1268	→	1302
  1151	→	517
  429	→	1310
  1525	→	371
  964	→	216
  32	→	146
  32	→	275
  917	→	175
  29	→	7
  29	→	154
  29	→	31
  29	→	208
  29	→	429
  29	→	407
  29	→	330
  29	→	109
  29	→	358
  29	→	100
  29	→	332
  29	→	229
  29	→	1329
  29	→	1251
  29	→	1335
  29	→	1264
  29	→	1163
  29	→	1262
  29	→	1525
  29	→	1384
  29	→	1556
  1335	→	407
  1674	→	38
  263	→	1054
  263	→	1058
  263	→	1655
  1057	→	303
  750	→	100
  356	→	1144
  1333	→	38
  338	→	140
  1156	→	1408
  1156	→	1557
  152	→	674
  152	→	695
  152	→	985
  152	→	1239
  1089	→	358
  1648	→	1458
  214	→	139
  229	→	350
  1007	→	1275
  1007	→	1294
  1163	→	100
  1169	→	123
  387	→	53
  1546	→	38
  915	→	175
  1578	→	31
  1409	→	53
  1409	→	1545
  1704	→	1458
  1280	→	303
  1209	→	184
  1544	→	38
  84	→	1049
  84	→	1056
  84	→	1475
  998	→	251
  998	→	1146
  1008	→	1154
  1008	→	1508
  956	→	208
  436	→	140
  1249	→	428
  1249	→	248
  1249	→	215
  1249	→	416
  1249	→	207
  1327	→	371
  705	→	208
  815	→	123
  1577	→	1681
  1577	→	1683
  1577	→	1691
  1577	→	1695
  1577	→	1697
  1577	→	1699
  39	→	749
  39	→	1079
  39	→	1092
  39	→	1329
  39	→	1525
  184	→	437
  1411	→	1185
  988	→	28
  57	→	339
  1710	→	100
  1294	→	1381
  1294	→	1518
  1294	→	1522
  1325	→	28
  108	→	39
  919	→	175
  919	→	1111
  1706	→	28
  1714	→	1458
  1276	→	303
  110	→	1222
  110	→	207
  110	→	206
  110	→	99
  110	→	30
  110	→	19
  110	→	55
  110	→	122
  110	→	7
  110	→	216
  1076	→	1349
  1055	→	303
  275	→	920
  456	→	710
  1681	→	1709
  1681	→	1715
  1681	→	1717
  1048	→	31
  1048	→	372
  1048	→	209
  1048	→	1329
  1048	→	1311
  1048	→	333
  1048	→	1525
  255	→	916
  255	→	1132
  255	→	1410
  55	→	1176
  55	→	1334
  1646	→	303
  243	→	191
  1295	→	20
  1636	→	283
  1662	→	28
  20	→	45
  20	→	283
  20	→	7
  20	→	517
  20	→	1151
  1238	→	28
  1159	→	69
  1159	→	1208
  107	→	1088
  31	→	154
  31	→	371
  31	→	7
  1668	→	371
  1403	→	53
  1403	→	1537
  40	→	7
  40	→	31
  40	→	208
  40	→	283
  40	→	45
  40	→	20
  40	→	1329
  40	→	1149
  40	→	1525
  123	→	175
  123	→	228
  123	→	379
  1077	→	1218
  1077	→	1265
  1077	→	1277
  1077	→	1473
  826	→	56
  826	→	206
  826	→	99
  826	→	30
  826	→	19
  826	→	55
  826	→	122
  826	→	7
  826	→	110
  826	→	1171
  1078	→	447
  1078	→	379
  1078	→	175
  1078	→	206
  1078	→	99
  1078	→	30
  1078	→	19
  1078	→	55
  1078	→	122
  1078	→	7
  1078	→	228
  1078	→	123
  1078	→	417
  1078	→	1407
  1009	→	156
  1009	→	407
  1009	→	330
  1009	→	7
  1009	→	109
  1009	→	358
  1009	→	100
  1009	→	429
  654	→	53
  1656	→	1458
  1331	→	38
  1112	→	1096
  1509	→	1313
  101	→	257
  1223	→	212
  1154	→	1402
  1154	→	1551
  770	→	1269
  770	→	1281
  770	→	1481
  1323	→	28
  1507	→	1313
  416	→	1152
  416	→	1506
  139	→	1271
  139	→	1457
  1278	→	303
  1515	→	1313
  1194	→	229
  1194	→	1310
  1194	→	100
  1194	→	208
  1194	→	154
  1194	→	371
  1194	→	1328
  1194	→	1162
  1194	→	1261
  1194	→	1168
  1194	→	1148
  1194	→	1176
  1194	→	122
  1194	→	55
  1194	→	19
  1194	→	30
  1194	→	99
  1194	→	206
  1194	→	7
  1194	→	31
  1194	→	429
  1194	→	332
  1194	→	29
  748	→	100
  1700	→	1251
  1329	→	371
  423	→	139
  423	→	955
  1676	→	407
  1161	→	100
  76	→	38
  235	→	747
  675	→	69
  1348	→	428
  1348	→	248
  1348	→	155
  1348	→	215
  1348	→	416
  1348	→	207
  309	→	181
  1654	→	1458
  1157	→	56
  1370	→	495
  1622	→	1251
  161	→	1038
  21	→	77
  21	→	310
  552	→	428
  552	→	248
  552	→	155
  552	→	206
  552	→	99
  552	→	30
  552	→	19
  552	→	55
  552	→	122
  552	→	7
  552	→	215
  552	→	416
  552	→	207
  1564	→	407
  141	→	7
  141	→	56
  141	→	110
  141	→	428
  141	→	248
  141	→	215
  141	→	416
  141	→	207
  141	→	155
  141	→	21
  141	→	331
  141	→	1171
  141	→	518
  526	→	208
  526	→	231
  824	→	1451
  824	→	1467
  207	→	215
  207	→	248
  207	→	416
  207	→	428
  1311	→	112
  1382	→	100
  1610	→	53
  1610	→	1673
  648	→	1066
  1193	→	1369
  1193	→	1571
  1193	→	1577
  1193	→	1593
  1193	→	1599
  1193	→	1619
  1193	→	1621
  337	→	761
  337	→	792
  337	→	1090
  1571	→	1689
  1571	→	1705
  1571	→	1707
  153	→	140
  109	→	1404
  109	→	1563
  1456	→	303
  345	→	190
  986	→	28
  54	→	7
  54	→	428
  54	→	248
  54	→	155
  54	→	215
  54	→	416
  54	→	207
  54	→	216
  54	→	303
  54	→	132
  54	→	418
  54	→	176
  54	→	69
  54	→	183
  54	→	56
  54	→	1171
  455	→	543
  1282	→	303
  1450	→	303
  1205	→	447
  1205	→	494
  1205	→	228
  1205	→	7
  1205	→	175
  1205	→	379
  1205	→	123
  1205	→	417
  1205	→	1407
  1131	→	407
  1047	→	1156
  1047	→	1514
  1364	→	28
  230	→	237
  1297	→	310
  1566	→	28
  264	→	191
  1192	→	1635
  1192	→	1711
  1192	→	1713
  1337	→	407
  1346	→	1701
  1346	→	1703
  1684	→	495
  717	→	1267
  717	→	1279
  717	→	1479
  53	→	918
  53	→	1134
  117	→	84
  1540	→	38
  1347	→	1455
  1347	→	1485
  1347	→	1647
  28	→	454
  28	→	516
  28	→	814
  28	→	816
  28	→	999
  28	→	1250
  1594	→	123
  1501	→	1313
  1538	→	38
  802	→	209
  359	→	1251
  359	→	1163
  359	→	1264
  359	→	1335
  359	→	1262
  359	→	1556
  359	→	1384
  1452	→	303
  1155	→	56
  1059	→	20
  504	→	231
  504	→	208
  1063	→	335
  1692	→	123
  63	→	1094
  357	→	84
  357	→	961
  1270	→	283
  1270	→	1304
  1600	→	132
  1698	→	100
  1145	→	183
  1143	→	183
  1177	→	53
  1177	→	1330
  85	→	7
  85	→	31
  85	→	208
  85	→	372
  85	→	209
  85	→	207
  85	→	216
  85	→	447
  85	→	379
  85	→	175
  85	→	228
  85	→	123
  85	→	417
  85	→	155
  85	→	1329
  85	→	1525
  85	→	1407
  1482	→	1458
  140	→	693
  140	→	987
  140	→	1195
  100	→	109
  100	→	330
  100	→	358
  100	→	407
  1517	→	1313
  1219	→	208
  1432	→	52
  1432	→	1565
  236	→	28
  1556	→	407
  1091	→	371
  282	→	84
  7	→	19
  7	→	30
  7	→	55
  7	→	99
  7	→	122
  7	→	206
  1006	→	1645
  1006	→	1653
  1712	→	303
  694	→	69
  694	→	931
  1080	→	1069
  417	→	447
  417	→	379
  417	→	175
  417	→	206
  417	→	99
  417	→	30
  417	→	19
  417	→	55
  417	→	122
  417	→	7
  417	→	228
  417	→	123
  417	→	1177
  417	→	1325
  417	→	1169
  417	→	1521
  1204	→	1371
  1204	→	1500
  113	→	1062
  182	→	161
  1207	→	1196
  30	→	1148
  30	→	1150
  30	→	1168
  30	→	1170
  30	→	1261
  30	→	1263
  962	→	208
  1179	→	53
  1179	→	1332
  64	→	39
  1305	→	310
  1321	→	1259
  453	→	316
  1133	→	407
  162	→	28
  1384	→	100
  1100	→	461
  1572	→	20
  825	→	1158
  825	→	1206
  825	→	1237
  158	→	1363
  1718	→	371
  256	→	140
  1372	→	56
  771	→	372
  771	→	371
  771	→	7
  771	→	154
  771	→	31
  771	→	1329
  771	→	1525
  1149	→	20
  1272	→	303
  1203	→	1431
  1486	→	20
  718	→	31
  718	→	208
  718	→	1329
  718	→	1525
  1523	→	371
  1148	→	1383
  1148	→	1520
  1148	→	1524
  242	→	1068
  1260	→	156
  1260	→	429
  1260	→	1556
  1464	→	1191
  1476	→	1458
  462	→	53
  1407	→	53
  1407	→	1543
  1153	→	56
  1474	→	1458
  1696	→	132
  1266	→	283
  1266	→	1296
  1682	→	20
  1093	→	371
  131	→	28
  1058	→	1160
  1058	→	1322
  1058	→	1326
  1708	→	371
  1264	→	100
  1620	→	100
  378	→	130
  422	→	1142
  422	→	1338
  932	→	997
  1171	→	132
  19	→	1162
  19	→	1324
  19	→	1328
  935	→	263
  1050	→	1039
  1050	→	1060
  1065	→	112
  1480	→	1458
  660	→	647
  1552	→	407
  1716	→	28
  317	→	39
  1152	→	1406
  1152	→	1555
  1558	→	407
  551	→	1178
  551	→	1336
  1350	→	183
  930	→	281
  442	→	280
  1371	→	1609
  1371	→	1675
  1521	→	28
  1702	→	303
  56	→	69
  56	→	132
  56	→	183
  56	→	303
  56	→	7
  1468	→	1458
  1588	→	100
  151	→	914
  151	→	1130
  151	→	1184
  1485	→	1587
  1485	→	1661
  1485	→	1667
  262	→	1449
  262	→	1465
  191	→	659
  191	→	963
  191	→	1516
  1147	→	439
  192	→	7
  192	→	447
  192	→	379
  192	→	175
  192	→	228
  192	→	123
  192	→	417
  192	→	428
  192	→	248
  192	→	215
  192	→	416
  192	→	207
  192	→	156
  192	→	407
  192	→	330
  192	→	109
  192	→	358
  192	→	100
  192	→	429
  192	→	31
  192	→	372
  192	→	209
  192	→	1329
  192	→	1311
  192	→	333
  192	→	1251
  192	→	1163
  192	→	1264
  192	→	1335
  192	→	1262
  192	→	1407
  192	→	1556
  192	→	1384
  192	→	1525
  1061	→	310
  415	→	84
  228	→	494
  1262	→	1251
  156	→	1064
  1135	→	407
  1466	→	1458
  291	→	191
  1690	→	100
  435	→	646
  435	→	1312
  1519	→	28
  11(71)	→	72
  11(260)	→	261
  11(156)	→	157
  11(123)	→	124
  11(36)	→	37
  11(99)	→	100
  11(51)	→	52
  11(187)	→	188
  11(1039)	→	1040
  11(1006)	→	1007
  11(263)	→	264
  11(749)	→	750
  11(820)	→	821
  11(1074)	→	1075
  11(1619)	→	1620
  11(819)	→	820
  11(381)	→	382
  11(1689)	→	1690
  11(1336)	→	1337
  11(1132)	→	1133
  11(106)	→	107
  11(761)	→	762
  11(155)	→	156
  11(1381)	→	1382
  11(354)	→	355
  11(1130)	→	1131
  11(1709)	→	1710
  11(763)	→	764
  11(1263)	→	1264
  11(1675)	→	1676
  11(1555)	→	1556
  11(1097)	→	1098
  11(450)	→	451
  11(650)	→	651
  11(1007)	→	1008
  11(61)	→	62
  11(136)	→	137
  11(1045)	→	1046
  11(289)	→	290
  11(407)	→	408
  11(999)	→	1000
  11(449)	→	450
  11(252)	→	253
  11(78)	→	79
  11(315)	→	316
  11(59)	→	60
  11(134)	→	135
  11(711)	→	712
  11(262)	→	263
  11(232)	→	233
  11(340)	→	341
  11(652)	→	653
  11(1096)	→	1097
  11(32)	→	33
  11(1563)	→	1564
  11(1383)	→	1384
  11(110)	→	111
  11(747)	→	748
  11(1557)	→	1558
  11(281)	→	282
  11(1162)	→	1163
  11(818)	→	819
  11(1004)	→	1005
  11(33)	→	34
  11(177)	→	178
  11(1334)	→	1335
  11(209)	→	210
  11(770)	→	771
  11(420)	→	421
  11(283)	→	284
  11(1587)	→	1588
  11(135)	→	136
  11(717)	→	718
  11(1697)	→	1698
  11(429)	→	430
  11(84)	→	85
  11(549)	→	550
  11(139)	→	140
  11(310)	→	311
  11(380)	→	381
  11(428)	→	429
  11(1134)	→	1135
  11(331)	→	332
  11(239)	→	240
  11(133)	→	134
  11(363)	→	364
  11(125)	→	126
  11(1088)	→	1089
  11(38)	→	39
  11(1077)	→	1078
  11(1551)	→	1552
  11(824)	→	825
  11(821)	→	822
  11(1160)	→	1161
  11(147)	→	148
  11(148)	→	149
  11(69)	→	70
  11(222)	→	223
  11(161)	→	162
  22(1317)	→	1318
  22(1342)	→	1343
  22(1246)	→	1247
  22(1197)	→	1198
  22(1463)	→	1464
  22(1243)	→	1244
  22(498)	→	499
  22(1318)	→	1319
  22(1184)	→	1185
  22(1204)	→	1205
  22(1462)	→	1463
  22(1343)	→	1344
  22(920)	→	921
  22(1201)	→	1202
  22(520)	→	521
  22(699)	→	700
  22(1248)	→	1249
  22(697)	→	698
  22(1341)	→	1342
  22(1239)	→	1240
  22(1410)	→	1411
  22(1314)	→	1315
  22(1259)	→	1260
  22(1458)	→	1459
  22(1252)	→	1253
  02(521)	→	522
  02(702)	→	703
  02(799)	→	800
  02(1186)	→	1187
  02(1345)	→	1346
  02(499)	→	500
  02(796)	→	797
  02(795)	→	796
  02(525)	→	526
  02(1240)	→	1241
  02(922)	→	923
  02(1202)	→	1203
  02(1253)	→	1254
  02(1199)	→	1200
  02(1193)	→	1194
  02(929)	→	930
  02(503)	→	504
  02(1460)	→	1461
  12(801)	→	802
  12(1621)	→	1622
  12(1250)	→	1251
  12(1261)	→	1262
  12(1257)	→	1258
  12(698)	→	699
  12(928)	→	929
  12(1315)	→	1316
  12(696)	→	697
  12(923)	→	924
  12(1200)	→	1201
  12(1244)	→	1245
  12(1347)	→	1348
  12(1192)	→	1193
  12(1258)	→	1259
  12(794)	→	795
  12(1187)	→	1188
  12(1346)	→	1347
  12(1699)	→	1700
  12(703)	→	704
  12(792)	→	793
  12(1255)	→	1256
  41(220)	→	221
  41(1296)	→	1297
  41(159)	→	160
  41(1695)	→	1696
  41(659)	→	660
  41(1040)	→	1041
  41(431)	→	432
  41(1279)	→	1280
  41(128)	→	129
  41(548)	→	549
  41(1711)	→	1712
  41(221)	→	222
  41(1277)	→	1278
  41(101)	→	102
  41(113)	→	114
  41(547)	→	548
  41(255)	→	256
  41(20)	→	21
  41(551)	→	552
  41(114)	→	115
  41(183)	→	184
  41(1170)	→	1171
  41(1142)	→	1143
  41(1599)	→	1600
  41(418)	→	419
  41(766)	→	767
  41(767)	→	768
  41(1158)	→	1159
  41(275)	→	276
  41(217)	→	218
  41(712)	→	713
  41(175)	→	176
  41(50)	→	51
  41(1304)	→	1305
  41(284)	→	285
  41(285)	→	286
  41(37)	→	38
  41(151)	→	152
  41(1060)	→	1061
  41(79)	→	80
  41(693)	→	694
  41(210)	→	211
  41(1449)	→	1450
  41(1041)	→	1042
  41(179)	→	180
  41(248)	→	249
  41(1208)	→	1209
  41(646)	→	647
  41(1371)	→	1372
  41(341)	→	342
  41(816)	→	817
  41(769)	→	770
  41(1144)	→	1145
  41(385)	→	386
  41(1156)	→	1157
  41(63)	→	64
  41(1455)	→	1456
  41(460)	→	461
  41(49)	→	50
  41(674)	→	675
  41(1152)	→	1153
  41(1271)	→	1272
  41(1054)	→	1055
  41(216)	→	217
  41(259)	→	260
  41(362)	→	363
  41(417)	→	418
  41(1003)	→	1004
  41(138)	→	139
  41(304)	→	305
  41(382)	→	383
  41(364)	→	365
  41(55)	→	56
  41(1451)	→	1452
  41(1701)	→	1702
  41(1645)	→	1646
  41(384)	→	385
  41(25)	→	26
  41(1349)	→	1350
  41(105)	→	106
  41(823)	→	824
  41(26)	→	27
  41(461)	→	462
  41(109)	→	110
  41(1056)	→	1057
  41(1281)	→	1282
  41(218)	→	219
  41(53)	→	54
  41(1302)	→	1303
  41(249)	→	250
  41(361)	→	362
  41(180)	→	181
  41(344)	→	345
  41(1275)	→	1276
  41(762)	→	763
  41(455)	→	456
  41(1154)	→	1155
  41(150)	→	151
  41(27)	→	28
  41(116)	→	117
  41(931)	→	932
  41(1098)	→	1099
  41(278)	→	279
  41(181)	→	182
  30(7)	→	7
  10(7)	→	7
  52(1344)	→	1345
  52(1241)	→	1242
  52(1203)	→	1204
  52(1256)	→	1257
  52(1320)	→	1321
  52(701)	→	702
  52(1242)	→	1243
  20(7)	→	7
  31(19)	→	20
  31(933)	→	934
  31(1543)	→	1544
  31(21)	→	22
  31(100)	→	101
  31(1058)	→	1059
  31(287)	→	288
  31(374)	→	375
  31(372)	→	373
  31(1332)	→	1333
  31(1099)	→	1100
  31(716)	→	717
  31(647)	→	648
  31(242)	→	243
  31(146)	→	147
  31(157)	→	158
  31(1000)	→	1001
  31(56)	→	57
  31(360)	→	361
  31(1269)	→	1270
  31(411)	→	412
  31(1545)	→	1546
  31(1072)	→	1073
  31(1095)	→	1096
  31(1265)	→	1266
  31(39)	→	40
  31(22)	→	23
  31(1485)	→	1486
  31(653)	→	654
  31(1070)	→	1071
  31(451)	→	452
  31(107)	→	108
  31(1539)	→	1540
  31(1673)	→	1674
  31(997)	→	998
  31(83)	→	84
  31(235)	→	236
  31(1681)	→	1682
  31(383)	→	384
  31(350)	→	351
  31(314)	→	315
  31(1111)	→	1112
  31(1148)	→	1149
  31(1571)	→	1572
  31(240)	→	241
  31(102)	→	103
  31(306)	→	307
  31(62)	→	63
  31(454)	→	455
  31(413)	→	414
  31(1038)	→	1039
  31(1537)	→	1538
  31(158)	→	159
  31(379)	→	380
  31(254)	→	255
  31(185)	→	186
  31(250)	→	251
  31(1635)	→	1636
  31(1043)	→	1044
  31(212)	→	213
  31(1330)	→	1331
  31(313)	→	314
  31(1049)	→	1050
  31(377)	→	378
  31(352)	→	353
  31(434)	→	435
  31(1294)	→	1295
  31(457)	→	458
  31(412)	→	413
  31(253)	→	254
  31(359)	→	360
  31(178)	→	179
  31(337)	→	338
  31(73)	→	74
  31(1267)	→	1268
  31(421)	→	422
  31(456)	→	457
  31(437)	→	438
  01(1524)	→	1525
  01(1310)	→	1311
  01(176)	→	177
  01(376)	→	377
  01(765)	→	766
  01(934)	→	935
  01(132)	→	133
  01(1218)	→	1219
  01(333)	→	334
  01(48)	→	49
  01(77)	→	78
  01(1064)	→	1065
  01(60)	→	61
  01(764)	→	765
  01(410)	→	411
  01(305)	→	306
  01(230)	→	231
  01(189)	→	190
  01(1090)	→	1091
  01(432)	→	433
  01(137)	→	138
  01(961)	→	962
  01(544)	→	545
  01(233)	→	234
  01(312)	→	313
  01(817)	→	818
  01(1667)	→	1668
  01(1044)	→	1045
  01(24)	→	25
  01(459)	→	460
  01(258)	→	259
  01(1577)	→	1578
  01(46)	→	47
  01(1042)	→	1043
  01(365)	→	366
  01(648)	→	649
  01(1328)	→	1329
  01(186)	→	187
  01(280)	→	281
  01(373)	→	374
  01(447)	→	448
  01(768)	→	769
  01(710)	→	711
  01(111)	→	112
  01(228)	→	229
  01(1002)	→	1003
  01(75)	→	76
  01(30)	→	31
  01(316)	→	317
  01(651)	→	652
  01(1326)	→	1327
  01(1717)	→	1718
  01(124)	→	125
  01(286)	→	287
  01(129)	→	130
  01(822)	→	823
  01(371)	→	372
  01(28)	→	29
  01(1707)	→	1708
  01(208)	→	209
  01(546)	→	547
  01(955)	→	956
  01(1522)	→	1523
  01(1092)	→	1093
  01(1069)	→	1070
  01(288)	→	289
  01(433)	→	434
  01(115)	→	116
  01(234)	→	235
  01(207)	→	208
  01(332)	→	333
  01(57)	→	58
  01(112)	→	113
  50(7)	→	7
  40(7)	→	7
  51(237)	→	238
  51(1005)	→	1006
  51(408)	→	409
  51(375)	→	376
  51(277)	→	278
  51(276)	→	277
  51(154)	→	155
  51(52)	→	53
  51(126)	→	127
  51(206)	→	207
  51(219)	→	220
  51(229)	→	230
  51(356)	→	357
  51(103)	→	104
  51(422)	→	423
  51(152)	→	153
  51(355)	→	356
  51(34)	→	35
  51(261)	→	262
  51(215)	→	216
  51(1076)	→	1077
  51(1431)	→	1432
  51(190)	→	191
  51(74)	→	75
  51(825)	→	826
  51(963)	→	964
  51(80)	→	81
  51(251)	→	252
  51(550)	→	551
  51(713)	→	714
  51(140)	→	141
  51(448)	→	449
  51(330)	→	331
  51(441)	→	442
  51(1075)	→	1076
  21(1324)	→	1325
  21(160)	→	161
  21(1237)	→	1238
  21(72)	→	73
  21(308)	→	309
  21(82)	→	83
  21(1406)	→	1407
  21(1565)	→	1566
  21(290)	→	291
  21(211)	→	212
  21(1066)	→	1067
  21(1404)	→	1405
  21(985)	→	986
  21(188)	→	189
  21(409)	→	410
  21(419)	→	420
  21(1322)	→	1323
  21(358)	→	359
  21(649)	→	650
  21(31)	→	32
  21(543)	→	544
  21(191)	→	192
  21(23)	→	24
  21(814)	→	815
  21(1408)	→	1409
  21(1073)	→	1074
  21(1402)	→	1403
  21(334)	→	335
  21(343)	→	344
  21(1518)	→	1519
  21(914)	→	915
  21(439)	→	440
  21(47)	→	48
  21(122)	→	123
  21(1047)	→	1048
  21(45)	→	46
  21(307)	→	308
  21(1661)	→	1662
  21(336)	→	337
  21(435)	→	436
  21(342)	→	343
  21(1222)	→	1223
  21(458)	→	459
  21(932)	→	933
  21(1146)	→	1147
  21(386)	→	387
  21(452)	→	453
  21(987)	→	988
  21(311)	→	312
  21(353)	→	354
  21(1068)	→	1069
  21(1176)	→	1177
  21(430)	→	431
  21(438)	→	439
  21(1609)	→	1610
  21(339)	→	340
  21(149)	→	150
  21(335)	→	336
  21(714)	→	715
  21(279)	→	280
  21(1079)	→	1080
  21(241)	→	242
  21(1178)	→	1179
  21(715)	→	716
  21(130)	→	131
  21(414)	→	415
  21(351)	→	352
  21(1094)	→	1095
  21(104)	→	105
  21(1062)	→	1063
  21(70)	→	71
  21(257)	→	258
  21(918)	→	919
  21(35)	→	36
  21(127)	→	128
  21(1363)	→	1364
  21(1001)	→	1002
  21(916)	→	917
  21(1705)	→	1706
  21(1520)	→	1521
  21(1008)	→	1009
  21(81)	→	82
  21(303)	→	304
  21(416)	→	417
  21(1168)	→	1169
  21(238)	→	239
  21(440)	→	441
  21(58)	→	59
  21(184)	→	185
  21(1071)	→	1072
  21(1691)	→	1692
  21(213)	→	214
  21(1046)	→	1047
  21(231)	→	232
  21(1593)	→	1594
  21(545)	→	546
  21(1715)	→	1716
  32(1313)	→	1314
  32(1369)	→	1370
  32(700)	→	701
  32(516)	→	517
  32(1247)	→	1248
  32(1188)	→	1189
  32(924)	→	925
  32(1198)	→	1199
  32(1340)	→	1341
  32(704)	→	705
  32(496)	→	497
  32(1245)	→	1246
  32(518)	→	519
  32(519)	→	520
  32(494)	→	495
  32(1683)	→	1684
  32(1461)	→	1462
  32(1150)	→	1151
  32(1251)	→	1252
  32(497)	→	498
  00(7)	→	7
  42(1457)	→	1458
  42(921)	→	922
  42(1655)	→	1656
  42(800)	→	801
  42(1196)	→	1197
  42(1195)	→	1196
  42(523)	→	524
  42(925)	→	926
  42(495)	→	496
  42(1516)	→	1517
  42(1473)	→	1474
  42(1479)	→	1480
  42(1339)	→	1340
  42(1514)	→	1515
  42(1508)	→	1509
  42(1506)	→	1507
  42(1338)	→	1339
  42(1713)	→	1714
  42(522)	→	523
  42(797)	→	798
  42(695)	→	696
  42(793)	→	794
  42(1185)	→	1186
  42(517)	→	518
  42(1481)	→	1482
  42(1459)	→	1460
  42(1191)	→	1192
  42(1254)	→	1255
  42(1465)	→	1466
  42(1319)	→	1320
  42(501)	→	502
  42(502)	→	503
  42(1316)	→	1317
  42(1206)	→	1207
  42(1312)	→	1313
  42(524)	→	525
  42(500)	→	501
  42(927)	→	928
  42(1467)	→	1468
  42(1653)	→	1654
  42(1500)	→	1501
  42(1190)	→	1191
  42(1647)	→	1648
  42(1189)	→	1190
  42(926)	→	927
  42(1703)	→	1704
  42(798)	→	799
  42(1475)	→	1476