YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(1(2(0(x0))))	→	0(1(0(x0)))
2(3(4(4(x0))))	→	0(3(4(x0)))
2(2(4(3(2(5(2(x0)))))))	→	0(3(0(0(0(x0)))))
3(2(2(0(4(1(3(0(x0))))))))	→	3(4(2(0(1(0(5(0(x0))))))))
2(2(2(3(0(1(2(2(5(x0)))))))))	→	0(1(1(1(3(5(2(5(x0))))))))
3(0(4(3(1(1(0(1(1(x0)))))))))	→	3(4(1(2(3(3(4(3(x0))))))))
2(4(2(0(3(5(0(3(2(4(x0))))))))))	→	0(0(0(1(0(1(3(2(x0))))))))
4(2(3(3(1(0(5(2(5(3(x0))))))))))	→	5(4(4(0(2(0(0(4(3(x0)))))))))
4(3(2(0(1(5(0(3(0(5(x0))))))))))	→	4(4(1(2(5(5(2(4(2(1(x0))))))))))
0(3(3(1(3(0(3(4(5(0(5(x0)))))))))))	→	0(3(4(1(5(2(0(2(1(3(x0))))))))))
5(3(4(0(4(4(0(5(2(2(0(x0)))))))))))	→	5(4(5(3(1(0(0(4(5(2(x0))))))))))
2(1(5(1(2(4(2(2(2(1(5(1(x0))))))))))))	→	2(1(3(2(5(1(2(0(2(3(4(x0)))))))))))
2(2(5(5(1(2(1(5(5(5(3(0(2(x0)))))))))))))	→	4(4(4(1(1(4(1(5(5(1(2(x0)))))))))))
3(3(5(1(5(4(2(3(2(1(0(0(2(0(x0))))))))))))))	→	4(3(0(3(5(1(1(3(1(5(4(3(1(x0)))))))))))))
2(3(3(0(3(3(3(1(4(2(0(5(4(1(2(2(x0))))))))))))))))	→	3(5(1(0(3(0(3(3(4(5(4(2(2(5(1(x0)))))))))))))))
3(5(4(3(2(3(0(3(5(2(4(4(1(0(5(4(x0))))))))))))))))	→	3(5(4(5(0(5(1(0(2(3(3(4(5(2(2(2(4(x0)))))))))))))))))
4(1(1(4(5(2(4(1(4(2(5(3(5(2(0(0(x0))))))))))))))))	→	4(3(0(2(3(3(5(4(4(0(0(0(5(4(2(3(x0))))))))))))))))
4(4(1(2(0(2(0(5(4(3(0(0(1(2(2(2(x0))))))))))))))))	→	4(5(4(2(4(1(0(4(0(1(1(2(4(4(4(x0)))))))))))))))
0(2(1(1(5(2(5(0(3(5(5(0(3(5(4(2(2(x0)))))))))))))))))	→	4(2(2(5(1(5(1(5(4(4(4(4(0(2(5(3(0(x0)))))))))))))))))
2(5(5(1(0(0(2(1(2(3(5(1(1(1(1(2(2(4(x0))))))))))))))))))	→	4(3(2(1(5(4(0(3(2(3(5(5(2(4(1(4(x0))))))))))))))))
2(5(5(3(4(2(0(0(2(0(4(0(4(4(2(5(4(0(x0))))))))))))))))))	→	5(1(1(4(0(5(5(2(5(0(1(2(4(2(4(4(x0))))))))))))))))
3(0(1(1(5(1(2(1(0(3(2(3(2(0(3(4(3(4(0(x0)))))))))))))))))))	→	1(5(3(0(5(4(4(0(0(4(1(3(4(3(1(4(1(x0)))))))))))))))))
3(3(5(4(4(1(5(5(2(1(5(4(4(5(1(0(5(3(1(x0)))))))))))))))))))	→	1(0(0(0(1(0(4(5(4(0(2(3(5(3(5(4(4(0(3(x0)))))))))))))))))))
3(5(2(2(4(2(0(3(4(4(3(5(4(4(1(4(5(2(4(x0)))))))))))))))))))	→	4(2(1(2(0(3(2(3(0(3(2(5(1(4(1(2(3(4(x0))))))))))))))))))
4(0(4(4(5(2(2(0(4(4(0(3(5(3(5(5(0(5(2(x0)))))))))))))))))))	→	5(2(3(3(2(2(0(4(4(1(5(5(3(4(2(3(5(2(x0))))))))))))))))))
4(2(2(4(3(4(4(3(1(3(2(2(2(0(1(2(5(4(1(x0)))))))))))))))))))	→	5(4(4(5(4(2(0(2(3(2(3(4(2(1(2(1(4(1(x0))))))))))))))))))
3(3(4(5(1(3(1(3(4(1(4(0(2(2(0(4(2(4(2(2(x0))))))))))))))))))))	→	1(0(1(4(3(3(4(4(4(3(5(0(1(2(0(2(3(3(x0))))))))))))))))))
3(5(2(0(2(0(4(5(2(1(4(2(5(0(5(2(5(3(2(5(x0))))))))))))))))))))	→	1(2(5(4(5(3(3(0(0(5(5(4(4(0(3(0(3(1(x0))))))))))))))))))
2(3(1(5(2(3(0(3(3(1(3(2(1(3(1(4(3(5(1(5(4(x0)))))))))))))))))))))	→	3(1(1(4(5(4(5(3(4(2(4(5(3(5(4(1(3(4(0(4(x0))))))))))))))))))))
2(4(1(3(0(5(2(2(2(4(4(5(2(0(3(4(5(1(5(5(0(x0)))))))))))))))))))))	→	4(3(5(4(2(4(5(1(0(2(3(5(5(0(4(4(5(3(3(5(1(x0)))))))))))))))))))))

Proof

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

0(2(1(0(x0))))	→	0(1(0(x0)))
4(4(3(2(x0))))	→	4(3(0(x0)))
2(5(2(3(4(2(2(x0)))))))	→	0(0(0(3(0(x0)))))
0(3(1(4(0(2(2(3(x0))))))))	→	0(5(0(1(0(2(4(3(x0))))))))
5(2(2(1(0(3(2(2(2(x0)))))))))	→	5(2(5(3(1(1(1(0(x0))))))))
1(1(0(1(1(3(4(0(3(x0)))))))))	→	3(4(3(3(2(1(4(3(x0))))))))
4(2(3(0(5(3(0(2(4(2(x0))))))))))	→	2(3(1(0(1(0(0(0(x0))))))))
3(5(2(5(0(1(3(3(2(4(x0))))))))))	→	3(4(0(0(2(0(4(4(5(x0)))))))))
5(0(3(0(5(1(0(2(3(4(x0))))))))))	→	1(2(4(2(5(5(2(1(4(4(x0))))))))))
5(0(5(4(3(0(3(1(3(3(0(x0)))))))))))	→	3(1(2(0(2(5(1(4(3(0(x0))))))))))
0(2(2(5(0(4(4(0(4(3(5(x0)))))))))))	→	2(5(4(0(0(1(3(5(4(5(x0))))))))))
1(5(1(2(2(2(4(2(1(5(1(2(x0))))))))))))	→	4(3(2(0(2(1(5(2(3(1(2(x0)))))))))))
2(0(3(5(5(5(1(2(1(5(5(2(2(x0)))))))))))))	→	2(1(5(5(1(4(1(1(4(4(4(x0)))))))))))
0(2(0(0(1(2(3(2(4(5(1(5(3(3(x0))))))))))))))	→	1(3(4(5(1(3(1(1(5(3(0(3(4(x0)))))))))))))
2(2(1(4(5(0(2(4(1(3(3(3(0(3(3(2(x0))))))))))))))))	→	1(5(2(2(4(5(4(3(3(0(3(0(1(5(3(x0)))))))))))))))
4(5(0(1(4(4(2(5(3(0(3(2(3(4(5(3(x0))))))))))))))))	→	4(2(2(2(5(4(3(3(2(0(1(5(0(5(4(5(3(x0)))))))))))))))))
0(0(2(5(3(5(2(4(1(4(2(5(4(1(1(4(x0))))))))))))))))	→	3(2(4(5(0(0(0(4(4(5(3(3(2(0(3(4(x0))))))))))))))))
2(2(2(1(0(0(3(4(5(0(2(0(2(1(4(4(x0))))))))))))))))	→	4(4(4(2(1(1(0(4(0(1(4(2(4(5(4(x0)))))))))))))))
2(2(4(5(3(0(5(5(3(0(5(2(5(1(1(2(0(x0)))))))))))))))))	→	0(3(5(2(0(4(4(4(4(5(1(5(1(5(2(2(4(x0)))))))))))))))))
4(2(2(1(1(1(1(5(3(2(1(2(0(0(1(5(5(2(x0))))))))))))))))))	→	4(1(4(2(5(5(3(2(3(0(4(5(1(2(3(4(x0))))))))))))))))
0(4(5(2(4(4(0(4(0(2(0(0(2(4(3(5(5(2(x0))))))))))))))))))	→	4(4(2(4(2(1(0(5(2(5(5(0(4(1(1(5(x0))))))))))))))))
0(4(3(4(3(0(2(3(2(3(0(1(2(1(5(1(1(0(3(x0)))))))))))))))))))	→	1(4(1(3(4(3(1(4(0(0(4(4(5(0(3(5(1(x0)))))))))))))))))
1(3(5(0(1(5(4(4(5(1(2(5(5(1(4(4(5(3(3(x0)))))))))))))))))))	→	3(0(4(4(5(3(5(3(2(0(4(5(4(0(1(0(0(0(1(x0)))))))))))))))))))
4(2(5(4(1(4(4(5(3(4(4(3(0(2(4(2(2(5(3(x0)))))))))))))))))))	→	4(3(2(1(4(1(5(2(3(0(3(2(3(0(2(1(2(4(x0))))))))))))))))))
2(5(0(5(5(3(5(3(0(4(4(0(2(2(5(4(4(0(4(x0)))))))))))))))))))	→	2(5(3(2(4(3(5(5(1(4(4(0(2(2(3(3(2(5(x0))))))))))))))))))
1(4(5(2(1(0(2(2(2(3(1(3(4(4(3(4(2(2(4(x0)))))))))))))))))))	→	1(4(1(2(1(2(4(3(2(3(2(0(2(4(5(4(4(5(x0))))))))))))))))))
2(2(4(2(4(0(2(2(0(4(1(4(3(1(3(1(5(4(3(3(x0))))))))))))))))))))	→	3(3(2(0(2(1(0(5(3(4(4(4(3(3(4(1(0(1(x0))))))))))))))))))
5(2(3(5(2(5(0(5(2(4(1(2(5(4(0(2(0(2(5(3(x0))))))))))))))))))))	→	1(3(0(3(0(4(4(5(5(0(0(3(3(5(4(5(2(1(x0))))))))))))))))))
4(5(1(5(3(4(1(3(1(2(3(1(3(3(0(3(2(5(1(3(2(x0)))))))))))))))))))))	→	4(0(4(3(1(4(5(3(5(4(2(4(3(5(4(5(4(1(1(3(x0))))))))))))))))))))
0(5(5(1(5(4(3(0(2(5(4(4(2(2(2(5(0(3(1(4(2(x0)))))))))))))))))))))	→	1(5(3(3(5(4(4(0(5(5(3(2(0(1(5(4(2(4(5(3(4(x0)))))))))))))))))))))

1.1 Bounds

The given TRS is match-bounded by 1. This is shown by the following automaton.

final states:

{339, 320, 303, 287, 272, 255, 239, 221, 204, 189, 175, 159, 145, 132, 117, 103, 91, 82, 71, 63, 56, 46, 37, 30, 24, 18, 10, 7, 5, 1}

transitions:

272 → 205

339 → 3

239 → 47

221 → 321

221 → 205

103 → 72

10 → 3

303 → 38

145 → 72

18 → 38

5 → 48

5 → 47

37 → 11

361 → 300

255 → 256

255 → 72

175 → 47

1 → 3

287 → 161

287 → 72

71 → 190

71 → 205

296 → 358

91 → 3

377 → 371

204 → 3

82 → 72

117 → 39

117 → 47

252 → 376

373 → 83

373 → 48

63 → 3

7 → 256

7 → 72

30 → 47

46 → 38

189 → 3

159 → 161

159 → 72

320 → 39

320 → 47

132 → 31

132 → 3

24 → 19

24 → 205

70 → 370

56 → 38

1₁(359) → 360

3₁(371) → 372

4₀(254) → 239

4₀(137) → 138

4₀(53) → 54

4₀(203) → 189

4₀(11) → 12

4₀(166) → 167

4₀(169) → 170

4₀(292) → 293

4₀(200) → 201

4₀(209) → 210

4₀(146) → 147

4₀(210) → 211

4₀(157) → 158

4₀(158) → 145

4₀(112) → 113

4₀(333) → 334

4₀(186) → 187

4₀(280) → 281

4₀(44) → 45

4₀(267) → 268

4₀(273) → 274

4₀(48) → 83

4₀(313) → 314

4₀(167) → 168

4₀(285) → 286

4₀(352) → 353

4₀(228) → 229

4₀(288) → 289

4₀(293) → 294

4₀(142) → 143

4₀(324) → 325

4₀(68) → 69

4₀(314) → 315

4₀(151) → 152

4₀(336) → 337

4₀(6) → 5

4₀(131) → 117

4₀(262) → 263

4₀(136) → 137

4₀(110) → 111

4₀(236) → 237

4₀(322) → 323

4₀(148) → 149

4₀(39) → 40

4₀(126) → 127

4₀(81) → 71

4₀(338) → 320

4₀(261) → 262

4₀(342) → 343

4₀(191) → 192

4₀(327) → 328

4₀(202) → 203

4₀(28) → 29

4₀(250) → 251

4₀(340) → 341

4₀(47) → 48

4₀(2) → 47

4₀(178) → 179

4₀(213) → 214

4₀(305) → 306

4₀(351) → 352

4₀(85) → 86

4₀(329) → 330

4₀(168) → 169

4₀(216) → 217

4₀(156) → 157

4₀(104) → 118

4₀(100) → 101

4₀(291) → 292

4₀(226) → 227

4₀(38) → 39

4₀(235) → 236

4₀(219) → 220

4₀(188) → 175

3₀(73) → 74

3₀(20) → 21

3₀(331) → 332

3₀(109) → 110

3₀(2) → 11

3₀(231) → 232

3₀(45) → 37

3₀(269) → 270

3₀(124) → 125

3₀(326) → 327

3₀(354) → 355

3₀(26) → 27

3₀(318) → 319

3₀(266) → 267

3₀(133) → 134

3₀(144) → 132

3₀(173) → 174

3₀(289) → 290

3₀(80) → 81

3₀(233) → 234

3₀(242) → 243

3₀(47) → 92

3₀(316) → 317

3₀(308) → 309

3₀(106) → 107

3₀(108) → 109

3₀(279) → 280

3₀(253) → 254

3₀(290) → 291

3₀(93) → 94

3₀(302) → 287

3₀(125) → 126

3₀(238) → 221

3₀(347) → 348

3₀(277) → 278

3₀(27) → 28

3₀(217) → 218

3₀(134) → 135

3₀(64) → 65

3₀(97) → 98

3₀(257) → 258

3₀(62) → 56

3₀(182) → 183

3₀(244) → 245

3₀(180) → 181

3₀(355) → 356

3₀(307) → 308

3₀(206) → 207

3₀(256) → 257

3₀(3) → 6

3₀(29) → 24

3₀(301) → 302

3₀(335) → 336

3₀(101) → 102

3₀(215) → 216

3₀(246) → 247

3₀(35) → 36

3₀(294) → 295

1₀(98) → 99

1₀(65) → 66

1₀(319) → 303

1₀(218) → 219

1₀(76) → 77

1₀(14) → 15

1₀(251) → 252

1₀(160) → 240

1₀(19) → 20

1₀(86) → 87

1₀(357) → 339

1₀(84) → 85

1₀(34) → 35

1₀(344) → 345

1₀(11) → 321

1₀(32) → 33

1₀(95) → 96

1₀(38) → 190

1₀(220) → 204

1₀(187) → 188

1₀(149) → 150

1₀(176) → 177

1₀(55) → 46

1₀(263) → 264

1₀(282) → 283

1₀(222) → 288

1₀(3) → 4

1₀(249) → 250

1₀(284) → 285

1₀(164) → 165

1₀(286) → 272

1₀(121) → 122

1₀(104) → 105

1₀(154) → 155

1₀(116) → 103

1₀(96) → 97

1₀(12) → 25

1₀(334) → 335

1₀(162) → 163

1₀(61) → 62

1₀(72) → 73

1₀(224) → 225

1₀(83) → 84

1₀(102) → 91

1₀(297) → 298

1₀(48) → 49

1₀(5) → 57

1₀(321) → 322

1₀(2) → 205

1₀(4) → 19

1₀(214) → 215

1₀(153) → 154

1₀(198) → 199

1₀(89) → 90

1₀(190) → 191

5₀(87) → 88

5₀(21) → 22

5₀(47) → 146

5₀(135) → 136

5₀(120) → 121

5₀(99) → 100

5₀(227) → 228

5₀(177) → 178

5₀(353) → 354

5₀(172) → 173

5₀(88) → 89

5₀(349) → 350

5₀(208) → 209

5₀(330) → 331

5₀(141) → 142

5₀(50) → 51

5₀(94) → 95

5₀(69) → 70

5₀(11) → 104

5₀(304) → 305

5₀(196) → 197

5₀(184) → 185

5₀(295) → 296

5₀(343) → 344

5₀(270) → 271

5₀(323) → 324

5₀(356) → 357

5₀(234) → 235

5₀(118) → 119

5₀(39) → 64

5₀(92) → 340

5₀(348) → 349

5₀(161) → 162

5₀(248) → 249

5₀(232) → 233

5₀(194) → 195

5₀(193) → 194

5₀(40) → 273

5₀(16) → 17

5₀(165) → 166

5₀(306) → 307

5₀(311) → 312

5₀(57) → 58

5₀(163) → 164

5₀(183) → 184

5₀(51) → 52

5₀(332) → 333

5₀(205) → 206

5₀(23) → 18

5₀(312) → 313

5₀(115) → 116

5₀(111) → 112

5₀(325) → 326

5₀(127) → 128

5₀(75) → 76

5₀(265) → 266

5₀(264) → 265

5₀(2) → 38

2₀(90) → 82

2₀(274) → 275

2₀(70) → 63

2₀(123) → 124

2₀(147) → 148

2₀(93) → 133

2₀(77) → 78

2₀(60) → 61

2₀(230) → 231

2₀(328) → 329

2₀(185) → 186

2₀(155) → 156

2₀(247) → 248

2₀(79) → 80

2₀(128) → 129

2₀(12) → 13

2₀(278) → 279

2₀(268) → 269

2₀(205) → 304

2₀(130) → 131

2₀(341) → 342

2₀(92) → 176

2₀(258) → 259

2₀(54) → 55

2₀(22) → 23

2₀(243) → 244

2₀(181) → 182

2₀(114) → 115

2₀(199) → 200

2₀(252) → 253

2₀(38) → 256

2₀(74) → 75

2₀(49) → 50

2₀(201) → 202

2₀(240) → 241

2₀(300) → 301

2₀(171) → 172

2₀(113) → 114

2₀(281) → 282

2₀(2) → 72

2₀(36) → 30

2₀(41) → 42

2₀(271) → 255

2₀(143) → 144

2₀(298) → 299

2₀(129) → 130

2₀(58) → 59

2₀(52) → 53

2₀(276) → 277

2₀(259) → 260

2₀(346) → 347

2₀(47) → 160

2₀(25) → 26

2₀(195) → 196

2₀(283) → 284

2₀(160) → 161

f6₀ → 2

0₀(2) → 3

0₀(337) → 338

0₀(317) → 318

0₀(237) → 238

0₀(275) → 276

0₀(299) → 300

0₀(9) → 7

0₀(197) → 198

0₀(105) → 106

0₀(260) → 261

0₀(67) → 68

0₀(170) → 171

0₀(309) → 310

0₀(310) → 311

0₀(225) → 226

0₀(350) → 351

0₀(152) → 153

0₀(107) → 108

0₀(43) → 44

0₀(92) → 93

0₀(4) → 1

0₀(8) → 9

0₀(222) → 223

0₀(138) → 139

0₀(150) → 151

0₀(315) → 316

0₀(223) → 224

0₀(3) → 31

0₀(17) → 10

0₀(192) → 193

0₀(6) → 8

0₀(211) → 212

0₀(245) → 246

0₀(66) → 67

0₀(140) → 141

0₀(241) → 242

0₀(139) → 140

0₀(345) → 346

0₀(33) → 34

0₀(15) → 16

0₀(205) → 222

0₀(42) → 43

0₀(40) → 41

0₀(174) → 159

0₀(212) → 213

0₀(229) → 230

0₀(78) → 79

0₀(59) → 60

0₀(31) → 32

0₀(179) → 180

0₀(13) → 14

0₀(296) → 297

0₀(207) → 208

0₀(122) → 123

0₀(119) → 120

4₁(372) → 373

0₁(360) → 361

0₁(358) → 359

0₁(376) → 377

0₁(370) → 371

272	→	205
339	→	3
239	→	47
221	→	321
221	→	205
103	→	72
10	→	3
303	→	38
145	→	72
18	→	38
5	→	48
5	→	47
37	→	11
361	→	300
255	→	256
255	→	72
175	→	47
1	→	3
287	→	161
287	→	72
71	→	190
71	→	205
296	→	358
91	→	3
377	→	371
204	→	3
82	→	72
117	→	39
117	→	47
252	→	376
373	→	83
373	→	48
63	→	3
7	→	256
7	→	72
30	→	47
46	→	38
189	→	3
159	→	161
159	→	72
320	→	39
320	→	47
132	→	31
132	→	3
24	→	19
24	→	205
70	→	370
56	→	38
1₁(359)	→	360
3₁(371)	→	372
4₀(254)	→	239
4₀(137)	→	138
4₀(53)	→	54
4₀(203)	→	189
4₀(11)	→	12
4₀(166)	→	167
4₀(169)	→	170
4₀(292)	→	293
4₀(200)	→	201
4₀(209)	→	210
4₀(146)	→	147
4₀(210)	→	211
4₀(157)	→	158
4₀(158)	→	145
4₀(112)	→	113
4₀(333)	→	334
4₀(186)	→	187
4₀(280)	→	281
4₀(44)	→	45
4₀(267)	→	268
4₀(273)	→	274
4₀(48)	→	83
4₀(313)	→	314
4₀(167)	→	168
4₀(285)	→	286
4₀(352)	→	353
4₀(228)	→	229
4₀(288)	→	289
4₀(293)	→	294
4₀(142)	→	143
4₀(324)	→	325
4₀(68)	→	69
4₀(314)	→	315
4₀(151)	→	152
4₀(336)	→	337
4₀(6)	→	5
4₀(131)	→	117
4₀(262)	→	263
4₀(136)	→	137
4₀(110)	→	111
4₀(236)	→	237
4₀(322)	→	323
4₀(148)	→	149
4₀(39)	→	40
4₀(126)	→	127
4₀(81)	→	71
4₀(338)	→	320
4₀(261)	→	262
4₀(342)	→	343
4₀(191)	→	192
4₀(327)	→	328
4₀(202)	→	203
4₀(28)	→	29
4₀(250)	→	251
4₀(340)	→	341
4₀(47)	→	48
4₀(2)	→	47
4₀(178)	→	179
4₀(213)	→	214
4₀(305)	→	306
4₀(351)	→	352
4₀(85)	→	86
4₀(329)	→	330
4₀(168)	→	169
4₀(216)	→	217
4₀(156)	→	157
4₀(104)	→	118
4₀(100)	→	101
4₀(291)	→	292
4₀(226)	→	227
4₀(38)	→	39
4₀(235)	→	236
4₀(219)	→	220
4₀(188)	→	175
3₀(73)	→	74
3₀(20)	→	21
3₀(331)	→	332
3₀(109)	→	110
3₀(2)	→	11
3₀(231)	→	232
3₀(45)	→	37
3₀(269)	→	270
3₀(124)	→	125
3₀(326)	→	327
3₀(354)	→	355
3₀(26)	→	27
3₀(318)	→	319
3₀(266)	→	267
3₀(133)	→	134
3₀(144)	→	132
3₀(173)	→	174
3₀(289)	→	290
3₀(80)	→	81
3₀(233)	→	234
3₀(242)	→	243
3₀(47)	→	92
3₀(316)	→	317
3₀(308)	→	309
3₀(106)	→	107
3₀(108)	→	109
3₀(279)	→	280
3₀(253)	→	254
3₀(290)	→	291
3₀(93)	→	94
3₀(302)	→	287
3₀(125)	→	126
3₀(238)	→	221
3₀(347)	→	348
3₀(277)	→	278
3₀(27)	→	28
3₀(217)	→	218
3₀(134)	→	135
3₀(64)	→	65
3₀(97)	→	98
3₀(257)	→	258
3₀(62)	→	56
3₀(182)	→	183
3₀(244)	→	245
3₀(180)	→	181
3₀(355)	→	356
3₀(307)	→	308
3₀(206)	→	207
3₀(256)	→	257
3₀(3)	→	6
3₀(29)	→	24
3₀(301)	→	302
3₀(335)	→	336
3₀(101)	→	102
3₀(215)	→	216
3₀(246)	→	247
3₀(35)	→	36
3₀(294)	→	295
1₀(98)	→	99
1₀(65)	→	66
1₀(319)	→	303
1₀(218)	→	219
1₀(76)	→	77
1₀(14)	→	15
1₀(251)	→	252
1₀(160)	→	240
1₀(19)	→	20
1₀(86)	→	87
1₀(357)	→	339
1₀(84)	→	85
1₀(34)	→	35
1₀(344)	→	345
1₀(11)	→	321
1₀(32)	→	33
1₀(95)	→	96
1₀(38)	→	190
1₀(220)	→	204
1₀(187)	→	188
1₀(149)	→	150
1₀(176)	→	177
1₀(55)	→	46
1₀(263)	→	264
1₀(282)	→	283
1₀(222)	→	288
1₀(3)	→	4
1₀(249)	→	250
1₀(284)	→	285
1₀(164)	→	165
1₀(286)	→	272
1₀(121)	→	122
1₀(104)	→	105
1₀(154)	→	155
1₀(116)	→	103
1₀(96)	→	97
1₀(12)	→	25
1₀(334)	→	335
1₀(162)	→	163
1₀(61)	→	62
1₀(72)	→	73
1₀(224)	→	225
1₀(83)	→	84
1₀(102)	→	91
1₀(297)	→	298
1₀(48)	→	49
1₀(5)	→	57
1₀(321)	→	322
1₀(2)	→	205
1₀(4)	→	19
1₀(214)	→	215
1₀(153)	→	154
1₀(198)	→	199
1₀(89)	→	90
1₀(190)	→	191
5₀(87)	→	88
5₀(21)	→	22
5₀(47)	→	146
5₀(135)	→	136
5₀(120)	→	121
5₀(99)	→	100
5₀(227)	→	228
5₀(177)	→	178
5₀(353)	→	354
5₀(172)	→	173
5₀(88)	→	89
5₀(349)	→	350
5₀(208)	→	209
5₀(330)	→	331
5₀(141)	→	142
5₀(50)	→	51
5₀(94)	→	95
5₀(69)	→	70
5₀(11)	→	104
5₀(304)	→	305
5₀(196)	→	197
5₀(184)	→	185
5₀(295)	→	296
5₀(343)	→	344
5₀(270)	→	271
5₀(323)	→	324
5₀(356)	→	357
5₀(234)	→	235
5₀(118)	→	119
5₀(39)	→	64
5₀(92)	→	340
5₀(348)	→	349
5₀(161)	→	162
5₀(248)	→	249
5₀(232)	→	233
5₀(194)	→	195
5₀(193)	→	194
5₀(40)	→	273
5₀(16)	→	17
5₀(165)	→	166
5₀(306)	→	307
5₀(311)	→	312
5₀(57)	→	58
5₀(163)	→	164
5₀(183)	→	184
5₀(51)	→	52
5₀(332)	→	333
5₀(205)	→	206
5₀(23)	→	18
5₀(312)	→	313
5₀(115)	→	116
5₀(111)	→	112
5₀(325)	→	326
5₀(127)	→	128
5₀(75)	→	76
5₀(265)	→	266
5₀(264)	→	265
5₀(2)	→	38
2₀(90)	→	82
2₀(274)	→	275
2₀(70)	→	63
2₀(123)	→	124
2₀(147)	→	148
2₀(93)	→	133
2₀(77)	→	78
2₀(60)	→	61
2₀(230)	→	231
2₀(328)	→	329
2₀(185)	→	186
2₀(155)	→	156
2₀(247)	→	248
2₀(79)	→	80
2₀(128)	→	129
2₀(12)	→	13
2₀(278)	→	279
2₀(268)	→	269
2₀(205)	→	304
2₀(130)	→	131
2₀(341)	→	342
2₀(92)	→	176
2₀(258)	→	259
2₀(54)	→	55
2₀(22)	→	23
2₀(243)	→	244
2₀(181)	→	182
2₀(114)	→	115
2₀(199)	→	200
2₀(252)	→	253
2₀(38)	→	256
2₀(74)	→	75
2₀(49)	→	50
2₀(201)	→	202
2₀(240)	→	241
2₀(300)	→	301
2₀(171)	→	172
2₀(113)	→	114
2₀(281)	→	282
2₀(2)	→	72
2₀(36)	→	30
2₀(41)	→	42
2₀(271)	→	255
2₀(143)	→	144
2₀(298)	→	299
2₀(129)	→	130
2₀(58)	→	59
2₀(52)	→	53
2₀(276)	→	277
2₀(259)	→	260
2₀(346)	→	347
2₀(47)	→	160
2₀(25)	→	26
2₀(195)	→	196
2₀(283)	→	284
2₀(160)	→	161
f6₀	→	2
0₀(2)	→	3
0₀(337)	→	338
0₀(317)	→	318
0₀(237)	→	238
0₀(275)	→	276
0₀(299)	→	300
0₀(9)	→	7
0₀(197)	→	198
0₀(105)	→	106
0₀(260)	→	261
0₀(67)	→	68
0₀(170)	→	171
0₀(309)	→	310
0₀(310)	→	311
0₀(225)	→	226
0₀(350)	→	351
0₀(152)	→	153
0₀(107)	→	108
0₀(43)	→	44
0₀(92)	→	93
0₀(4)	→	1
0₀(8)	→	9
0₀(222)	→	223
0₀(138)	→	139
0₀(150)	→	151
0₀(315)	→	316
0₀(223)	→	224
0₀(3)	→	31
0₀(17)	→	10
0₀(192)	→	193
0₀(6)	→	8
0₀(211)	→	212
0₀(245)	→	246
0₀(66)	→	67
0₀(140)	→	141
0₀(241)	→	242
0₀(139)	→	140
0₀(345)	→	346
0₀(33)	→	34
0₀(15)	→	16
0₀(205)	→	222
0₀(42)	→	43
0₀(40)	→	41
0₀(174)	→	159
0₀(212)	→	213
0₀(229)	→	230
0₀(78)	→	79
0₀(59)	→	60
0₀(31)	→	32
0₀(179)	→	180
0₀(13)	→	14
0₀(296)	→	297
0₀(207)	→	208
0₀(122)	→	123
0₀(119)	→	120
4₁(372)	→	373
0₁(360)	→	361
0₁(358)	→	359
0₁(376)	→	377
0₁(370)	→	371