YES(?,O(n^1)) 1154.25/297.08 YES(?,O(n^1)) 1154.25/297.08 1154.25/297.08 We are left with following problem, upon which TcT provides the 1154.25/297.08 certificate YES(?,O(n^1)). 1154.25/297.08 1154.25/297.08 Strict Trs: 1154.25/297.08 { 0(0(0(2(2(5(x1)))))) -> 1(3(2(1(4(2(0(1(4(0(x1)))))))))) 1154.25/297.08 , 0(0(1(x1))) -> 5(4(2(1(4(1(3(4(2(2(x1)))))))))) 1154.25/297.08 , 0(0(2(0(0(4(2(x1))))))) -> 1(3(4(1(0(0(5(5(2(4(x1)))))))))) 1154.25/297.08 , 0(0(2(0(2(4(x1)))))) -> 5(2(3(4(4(5(2(1(4(1(x1)))))))))) 1154.25/297.08 , 0(0(2(2(5(4(x1)))))) -> 1(4(5(5(5(2(4(4(4(3(x1)))))))))) 1154.25/297.08 , 0(0(4(3(0(1(5(x1))))))) -> 2(5(4(5(1(2(4(1(0(5(x1)))))))))) 1154.25/297.08 , 0(1(x1)) -> 2(0(3(4(3(1(1(2(1(3(x1)))))))))) 1154.25/297.08 , 0(1(x1)) -> 4(4(2(4(2(3(3(1(3(3(x1)))))))))) 1154.25/297.08 , 0(1(x1)) -> 4(4(4(2(1(0(3(4(1(4(x1)))))))))) 1154.25/297.08 , 0(1(0(0(0(4(2(x1))))))) -> 3(2(5(2(0(4(2(3(4(1(x1)))))))))) 1154.25/297.08 , 0(1(0(4(0(0(2(x1))))))) -> 5(5(3(4(2(0(5(2(2(3(x1)))))))))) 1154.25/297.08 , 0(1(0(4(0(1(x1)))))) -> 0(3(0(3(3(3(0(1(1(4(x1)))))))))) 1154.25/297.08 , 0(1(2(5(x1)))) -> 1(4(3(0(3(4(4(2(3(5(x1)))))))))) 1154.25/297.08 , 0(2(0(x1))) -> 3(0(0(3(2(2(2(4(1(3(x1)))))))))) 1154.25/297.08 , 0(2(0(0(1(x1))))) -> 0(2(2(0(5(4(4(3(4(1(x1)))))))))) 1154.25/297.08 , 0(2(0(4(1(x1))))) -> 2(3(0(3(2(4(2(0(4(1(x1)))))))))) 1154.25/297.08 , 0(2(2(1(x1)))) -> 3(0(5(2(1(1(2(2(3(1(x1)))))))))) 1154.25/297.08 , 0(2(3(1(0(2(4(x1))))))) -> 3(3(1(0(4(2(1(2(4(3(x1)))))))))) 1154.25/297.08 , 0(2(3(1(5(0(1(x1))))))) -> 4(5(5(3(4(1(0(4(2(2(x1)))))))))) 1154.25/297.08 , 0(2(4(0(2(4(x1)))))) -> 5(0(5(4(2(2(0(1(4(2(x1)))))))))) 1154.25/297.08 , 0(2(5(2(5(2(x1)))))) -> 3(2(1(1(1(1(5(1(4(3(x1)))))))))) 1154.25/297.08 , 0(3(0(5(0(2(x1)))))) -> 4(2(1(2(4(4(0(0(1(1(x1)))))))))) 1154.25/297.08 , 0(4(0(0(4(2(x1)))))) -> 0(2(2(3(5(4(4(3(1(4(x1)))))))))) 1154.25/297.08 , 0(4(5(4(x1)))) -> 1(1(5(4(1(2(4(1(4(3(x1)))))))))) 1154.25/297.08 , 1(1(0(4(0(4(x1)))))) -> 1(2(1(3(4(4(5(4(4(2(x1)))))))))) 1154.25/297.08 , 1(5(1(x1))) -> 1(5(3(2(4(3(0(3(2(4(x1)))))))))) 1154.25/297.08 , 2(0(0(1(3(5(x1)))))) -> 4(2(4(0(2(4(4(1(3(5(x1)))))))))) 1154.25/297.08 , 2(4(5(1(0(0(2(x1))))))) -> 4(3(1(2(1(3(4(1(5(1(x1)))))))))) 1154.25/297.08 , 2(5(0(0(3(5(x1)))))) -> 4(1(3(3(3(5(4(0(5(5(x1)))))))))) 1154.25/297.08 , 2(5(0(4(3(0(x1)))))) -> 2(4(1(2(2(0(5(5(2(0(x1)))))))))) 1154.25/297.08 , 2(5(4(0(0(1(x1)))))) -> 4(4(2(4(1(0(1(1(0(1(x1)))))))))) 1154.25/297.08 , 3(0(0(1(5(x1))))) -> 3(2(4(3(2(2(1(2(0(5(x1)))))))))) 1154.25/297.08 , 3(0(2(2(1(x1))))) -> 3(2(0(5(4(1(3(1(4(3(x1)))))))))) 1154.25/297.08 , 3(0(3(0(5(2(5(x1))))))) -> 3(3(1(2(3(3(1(2(1(5(x1)))))))))) 1154.25/297.08 , 3(1(5(1(1(5(x1)))))) -> 3(3(0(3(3(0(3(2(2(0(x1)))))))))) 1154.25/297.08 , 3(3(0(4(0(0(4(x1))))))) -> 3(3(3(1(1(5(4(4(5(4(x1)))))))))) 1154.25/297.08 , 3(3(5(0(1(x1))))) -> 3(2(4(1(1(0(5(1(2(4(x1)))))))))) 1154.25/297.08 , 3(3(5(0(1(5(2(x1))))))) -> 3(1(5(1(1(2(4(3(1(3(x1)))))))))) 1154.25/297.08 , 3(5(1(0(5(1(x1)))))) -> 5(3(0(1(3(1(0(5(3(4(x1)))))))))) 1154.25/297.08 , 4(5(1(0(x1)))) -> 2(0(3(2(4(2(5(2(2(2(x1)))))))))) 1154.25/297.08 , 5(0(2(0(5(1(5(x1))))))) -> 5(0(0(0(0(3(2(4(3(5(x1)))))))))) 1154.25/297.08 , 5(1(1(3(1(0(4(x1))))))) -> 5(1(2(3(1(4(4(5(3(3(x1)))))))))) 1154.25/297.08 , 5(2(3(5(2(0(2(x1))))))) -> 5(2(2(4(4(1(2(5(5(2(x1)))))))))) 1154.25/297.08 , 5(3(3(5(1(x1))))) -> 5(3(2(5(4(4(1(1(4(4(x1)))))))))) 1154.25/297.08 , 5(4(5(0(2(x1))))) -> 5(4(0(3(4(5(2(1(3(1(x1)))))))))) } 1154.25/297.08 Obligation: 1154.25/297.08 derivational complexity 1154.25/297.08 Answer: 1154.25/297.08 YES(?,O(n^1)) 1154.25/297.08 1154.25/297.08 The problem is match-bounded by 2. The enriched problem is 1154.25/297.08 compatible with the following automaton. 1154.25/297.08 { 0_0(1) -> 1 1154.25/297.08 , 0_1(1) -> 10 1154.25/297.08 , 0_1(2) -> 10 1154.25/297.08 , 0_1(8) -> 7 1154.25/297.08 , 0_1(11) -> 10 1154.25/297.08 , 0_1(17) -> 190 1154.25/297.08 , 0_1(22) -> 21 1154.25/297.08 , 0_1(23) -> 22 1154.25/297.08 , 0_1(26) -> 173 1154.25/297.08 , 0_1(33) -> 173 1154.25/297.08 , 0_1(34) -> 278 1154.25/297.08 , 0_1(44) -> 10 1154.25/297.08 , 0_1(51) -> 50 1154.25/297.08 , 0_1(52) -> 43 1154.25/297.08 , 0_1(104) -> 103 1154.25/297.08 , 0_1(125) -> 124 1154.25/297.08 , 0_1(132) -> 131 1154.25/297.08 , 0_1(135) -> 1 1154.25/297.08 , 0_1(135) -> 10 1154.25/297.08 , 0_1(135) -> 173 1154.25/297.08 , 0_1(135) -> 278 1154.25/297.08 , 0_1(137) -> 136 1154.25/297.08 , 0_1(141) -> 140 1154.25/297.08 , 0_1(143) -> 142 1154.25/297.08 , 0_1(148) -> 121 1154.25/297.08 , 0_1(149) -> 148 1154.25/297.08 , 0_1(165) -> 164 1154.25/297.08 , 0_1(169) -> 168 1154.25/297.08 , 0_1(182) -> 181 1154.25/297.08 , 0_1(191) -> 11 1154.25/297.08 , 0_1(196) -> 195 1154.25/297.08 , 0_1(197) -> 190 1154.25/297.08 , 0_1(208) -> 207 1154.25/297.08 , 0_1(209) -> 208 1154.25/297.08 , 0_1(215) -> 10 1154.25/297.08 , 0_1(234) -> 10 1154.25/297.08 , 0_1(239) -> 238 1154.25/297.08 , 0_1(250) -> 249 1154.25/297.08 , 0_1(267) -> 266 1154.25/297.08 , 0_1(272) -> 271 1154.25/297.08 , 0_1(276) -> 275 1154.25/297.08 , 0_1(284) -> 122 1154.25/297.08 , 0_1(293) -> 180 1154.25/297.08 , 0_1(296) -> 295 1154.25/297.08 , 0_1(306) -> 305 1154.25/297.08 , 0_1(315) -> 314 1154.25/297.08 , 0_1(319) -> 318 1154.25/297.08 , 0_1(324) -> 191 1154.25/297.08 , 0_1(325) -> 324 1154.25/297.08 , 0_1(326) -> 325 1154.25/297.08 , 0_1(356) -> 12 1154.25/297.08 , 0_2(60) -> 59 1154.25/297.08 , 0_2(69) -> 68 1154.25/297.08 , 0_2(110) -> 109 1154.25/297.08 , 0_2(117) -> 116 1154.25/297.08 , 0_2(155) -> 154 1154.25/297.08 , 0_2(156) -> 155 1154.25/297.08 , 0_2(246) -> 245 1154.25/297.08 , 0_2(371) -> 370 1154.25/297.08 , 0_2(380) -> 379 1154.25/297.08 , 0_2(389) -> 388 1154.25/297.08 , 0_2(398) -> 397 1154.25/297.08 , 0_2(407) -> 406 1154.25/297.08 , 0_2(479) -> 478 1154.25/297.08 , 0_2(493) -> 492 1154.25/297.08 , 0_2(507) -> 506 1154.25/297.08 , 0_2(514) -> 513 1154.25/297.08 , 0_2(521) -> 520 1154.25/297.08 , 0_2(528) -> 527 1154.25/297.08 , 0_2(529) -> 528 1154.25/297.08 , 0_2(542) -> 541 1154.25/297.08 , 0_2(550) -> 549 1154.25/297.08 , 0_2(559) -> 558 1154.25/297.08 , 1_0(1) -> 1 1154.25/297.08 , 1_1(1) -> 34 1154.25/297.08 , 1_1(2) -> 1 1154.25/297.08 , 1_1(2) -> 10 1154.25/297.08 , 1_1(2) -> 34 1154.25/297.08 , 1_1(2) -> 173 1154.25/297.08 , 1_1(2) -> 209 1154.25/297.08 , 1_1(2) -> 276 1154.25/297.08 , 1_1(2) -> 278 1154.25/297.08 , 1_1(2) -> 292 1154.25/297.08 , 1_1(5) -> 4 1154.25/297.08 , 1_1(9) -> 8 1154.25/297.08 , 1_1(10) -> 49 1154.25/297.08 , 1_1(14) -> 13 1154.25/297.08 , 1_1(16) -> 15 1154.25/297.08 , 1_1(21) -> 20 1154.25/297.08 , 1_1(25) -> 307 1154.25/297.08 , 1_1(26) -> 106 1154.25/297.08 , 1_1(33) -> 32 1154.25/297.08 , 1_1(34) -> 209 1154.25/297.08 , 1_1(41) -> 202 1154.25/297.08 , 1_1(42) -> 58 1154.25/297.08 , 1_1(43) -> 34 1154.25/297.08 , 1_1(47) -> 46 1154.25/297.08 , 1_1(49) -> 276 1154.25/297.08 , 1_1(50) -> 49 1154.25/297.08 , 1_1(51) -> 292 1154.25/297.08 , 1_1(56) -> 55 1154.25/297.08 , 1_1(57) -> 56 1154.25/297.08 , 1_1(77) -> 34 1154.25/297.08 , 1_1(84) -> 83 1154.25/297.08 , 1_1(103) -> 102 1154.25/297.08 , 1_1(106) -> 141 1154.25/297.08 , 1_1(133) -> 176 1154.25/297.08 , 1_1(147) -> 253 1154.25/297.08 , 1_1(163) -> 34 1154.25/297.08 , 1_1(176) -> 175 1154.25/297.08 , 1_1(177) -> 176 1154.25/297.08 , 1_1(179) -> 360 1154.25/297.08 , 1_1(181) -> 180 1154.25/297.08 , 1_1(185) -> 184 1154.25/297.08 , 1_1(190) -> 189 1154.25/297.08 , 1_1(197) -> 196 1154.25/297.08 , 1_1(198) -> 122 1154.25/297.08 , 1_1(199) -> 198 1154.25/297.08 , 1_1(200) -> 199 1154.25/297.08 , 1_1(201) -> 200 1154.25/297.08 , 1_1(203) -> 1 1154.25/297.08 , 1_1(204) -> 203 1154.25/297.08 , 1_1(214) -> 2 1154.25/297.08 , 1_1(217) -> 216 1154.25/297.08 , 1_1(229) -> 228 1154.25/297.08 , 1_1(255) -> 254 1154.25/297.08 , 1_1(257) -> 256 1154.25/297.08 , 1_1(260) -> 259 1154.25/297.08 , 1_1(261) -> 77 1154.25/297.08 , 1_1(268) -> 34 1154.25/297.08 , 1_1(269) -> 268 1154.25/297.08 , 1_1(274) -> 282 1154.25/297.08 , 1_1(275) -> 80 1154.25/297.08 , 1_1(277) -> 276 1154.25/297.08 , 1_1(278) -> 277 1154.25/297.08 , 1_1(283) -> 282 1154.25/297.08 , 1_1(287) -> 286 1154.25/297.08 , 1_1(291) -> 290 1154.25/297.08 , 1_1(299) -> 298 1154.25/297.08 , 1_1(300) -> 299 1154.25/297.08 , 1_1(304) -> 279 1154.25/297.08 , 1_1(305) -> 304 1154.25/297.08 , 1_1(308) -> 121 1154.25/297.08 , 1_1(310) -> 309 1154.25/297.08 , 1_1(311) -> 310 1154.25/297.08 , 1_1(316) -> 315 1154.25/297.08 , 1_1(318) -> 317 1154.25/297.08 , 1_1(329) -> 11 1154.25/297.08 , 1_1(332) -> 331 1154.25/297.08 , 1_1(338) -> 337 1154.25/297.08 , 1_1(345) -> 344 1154.25/297.08 , 1_1(346) -> 345 1154.25/297.08 , 1_2(64) -> 63 1154.25/297.08 , 1_2(65) -> 64 1154.25/297.08 , 1_2(67) -> 66 1154.25/297.08 , 1_2(73) -> 72 1154.25/297.08 , 1_2(74) -> 73 1154.25/297.08 , 1_2(76) -> 75 1154.25/297.08 , 1_2(92) -> 91 1154.25/297.08 , 1_2(100) -> 99 1154.25/297.08 , 1_2(109) -> 108 1154.25/297.08 , 1_2(113) -> 112 1154.25/297.08 , 1_2(116) -> 115 1154.25/297.08 , 1_2(120) -> 119 1154.25/297.08 , 1_2(162) -> 161 1154.25/297.08 , 1_2(219) -> 173 1154.25/297.08 , 1_2(220) -> 219 1154.25/297.08 , 1_2(223) -> 222 1154.25/297.08 , 1_2(226) -> 225 1154.25/297.08 , 1_2(240) -> 200 1154.25/297.08 , 1_2(353) -> 352 1154.25/297.08 , 1_2(354) -> 353 1154.25/297.08 , 1_2(355) -> 112 1154.25/297.08 , 1_2(364) -> 363 1154.25/297.08 , 1_2(366) -> 365 1154.25/297.08 , 1_2(375) -> 374 1154.25/297.08 , 1_2(376) -> 375 1154.25/297.08 , 1_2(378) -> 377 1154.25/297.08 , 1_2(384) -> 383 1154.25/297.08 , 1_2(385) -> 384 1154.25/297.08 , 1_2(387) -> 386 1154.25/297.08 , 1_2(393) -> 392 1154.25/297.08 , 1_2(394) -> 393 1154.25/297.08 , 1_2(396) -> 395 1154.25/297.08 , 1_2(402) -> 401 1154.25/297.08 , 1_2(403) -> 402 1154.25/297.08 , 1_2(405) -> 404 1154.25/297.08 , 1_2(411) -> 410 1154.25/297.08 , 1_2(412) -> 411 1154.25/297.08 , 1_2(414) -> 413 1154.25/297.08 , 1_2(422) -> 421 1154.25/297.08 , 1_2(430) -> 429 1154.25/297.08 , 1_2(438) -> 437 1154.25/297.08 , 1_2(446) -> 445 1154.25/297.08 , 1_2(454) -> 453 1154.25/297.08 , 1_2(478) -> 477 1154.25/297.08 , 1_2(482) -> 481 1154.25/297.08 , 1_2(492) -> 491 1154.25/297.08 , 1_2(496) -> 495 1154.25/297.08 , 1_2(506) -> 505 1154.25/297.08 , 1_2(510) -> 509 1154.25/297.08 , 1_2(513) -> 512 1154.25/297.08 , 1_2(517) -> 516 1154.25/297.08 , 1_2(518) -> 278 1154.25/297.08 , 1_2(535) -> 534 1154.25/297.08 , 1_2(536) -> 259 1154.25/297.08 , 1_2(536) -> 292 1154.25/297.08 , 1_2(544) -> 121 1154.25/297.08 , 1_2(553) -> 34 1154.25/297.08 , 1_2(553) -> 49 1154.25/297.08 , 1_2(553) -> 58 1154.25/297.08 , 1_2(553) -> 253 1154.25/297.08 , 1_2(553) -> 259 1154.25/297.08 , 1_2(553) -> 277 1154.25/297.08 , 1_2(553) -> 292 1154.25/297.08 , 1_2(553) -> 377 1154.25/297.08 , 2_0(1) -> 1 1154.25/297.08 , 2_1(1) -> 19 1154.25/297.08 , 2_1(2) -> 19 1154.25/297.08 , 2_1(4) -> 3 1154.25/297.08 , 2_1(7) -> 6 1154.25/297.08 , 2_1(10) -> 274 1154.25/297.08 , 2_1(13) -> 12 1154.25/297.08 , 2_1(18) -> 323 1154.25/297.08 , 2_1(19) -> 18 1154.25/297.08 , 2_1(26) -> 25 1154.25/297.08 , 2_1(27) -> 11 1154.25/297.08 , 2_1(32) -> 31 1154.25/297.08 , 2_1(34) -> 291 1154.25/297.08 , 2_1(39) -> 38 1154.25/297.08 , 2_1(41) -> 185 1154.25/297.08 , 2_1(42) -> 134 1154.25/297.08 , 2_1(43) -> 1 1154.25/297.08 , 2_1(43) -> 10 1154.25/297.08 , 2_1(43) -> 19 1154.25/297.08 , 2_1(43) -> 26 1154.25/297.08 , 2_1(43) -> 113 1154.25/297.08 , 2_1(43) -> 302 1154.25/297.08 , 2_1(48) -> 47 1154.25/297.08 , 2_1(49) -> 291 1154.25/297.08 , 2_1(50) -> 283 1154.25/297.08 , 2_1(58) -> 57 1154.25/297.08 , 2_1(77) -> 19 1154.25/297.08 , 2_1(79) -> 78 1154.25/297.08 , 2_1(81) -> 80 1154.25/297.08 , 2_1(102) -> 101 1154.25/297.08 , 2_1(121) -> 274 1154.25/297.08 , 2_1(122) -> 121 1154.25/297.08 , 2_1(124) -> 123 1154.25/297.08 , 2_1(127) -> 126 1154.25/297.08 , 2_1(131) -> 130 1154.25/297.08 , 2_1(134) -> 133 1154.25/297.08 , 2_1(135) -> 19 1154.25/297.08 , 2_1(147) -> 146 1154.25/297.08 , 2_1(151) -> 150 1154.25/297.08 , 2_1(152) -> 151 1154.25/297.08 , 2_1(153) -> 152 1154.25/297.08 , 2_1(163) -> 135 1154.25/297.08 , 2_1(164) -> 163 1154.25/297.08 , 2_1(171) -> 170 1154.25/297.08 , 2_1(173) -> 172 1154.25/297.08 , 2_1(175) -> 174 1154.25/297.08 , 2_1(178) -> 177 1154.25/297.08 , 2_1(179) -> 178 1154.25/297.08 , 2_1(184) -> 183 1154.25/297.08 , 2_1(194) -> 193 1154.25/297.08 , 2_1(195) -> 194 1154.25/297.08 , 2_1(203) -> 77 1154.25/297.08 , 2_1(205) -> 204 1154.25/297.08 , 2_1(218) -> 217 1154.25/297.08 , 2_1(228) -> 2 1154.25/297.08 , 2_1(236) -> 235 1154.25/297.08 , 2_1(251) -> 250 1154.25/297.08 , 2_1(256) -> 255 1154.25/297.08 , 2_1(268) -> 19 1154.25/297.08 , 2_1(270) -> 269 1154.25/297.08 , 2_1(271) -> 270 1154.25/297.08 , 2_1(274) -> 297 1154.25/297.08 , 2_1(281) -> 280 1154.25/297.08 , 2_1(282) -> 281 1154.25/297.08 , 2_1(288) -> 181 1154.25/297.08 , 2_1(292) -> 291 1154.25/297.08 , 2_1(312) -> 311 1154.25/297.08 , 2_1(320) -> 53 1154.25/297.08 , 2_1(322) -> 321 1154.25/297.08 , 2_1(328) -> 327 1154.25/297.08 , 2_1(330) -> 329 1154.25/297.08 , 2_1(335) -> 27 1154.25/297.08 , 2_1(339) -> 338 1154.25/297.08 , 2_1(341) -> 314 1154.25/297.08 , 2_1(360) -> 359 1154.25/297.08 , 2_2(2) -> 369 1154.25/297.08 , 2_2(34) -> 369 1154.25/297.08 , 2_2(59) -> 10 1154.25/297.08 , 2_2(59) -> 208 1154.25/297.08 , 2_2(59) -> 275 1154.25/297.08 , 2_2(59) -> 278 1154.25/297.09 , 2_2(66) -> 65 1154.25/297.09 , 2_2(68) -> 7 1154.25/297.09 , 2_2(75) -> 74 1154.25/297.09 , 2_2(87) -> 86 1154.25/297.09 , 2_2(89) -> 88 1154.25/297.09 , 2_2(95) -> 94 1154.25/297.09 , 2_2(97) -> 96 1154.25/297.09 , 2_2(108) -> 107 1154.25/297.09 , 2_2(113) -> 543 1154.25/297.09 , 2_2(115) -> 114 1154.25/297.09 , 2_2(158) -> 157 1154.25/297.09 , 2_2(159) -> 158 1154.25/297.09 , 2_2(160) -> 159 1154.25/297.09 , 2_2(224) -> 223 1154.25/297.09 , 2_2(243) -> 242 1154.25/297.09 , 2_2(248) -> 247 1154.25/297.09 , 2_2(349) -> 348 1154.25/297.09 , 2_2(355) -> 560 1154.25/297.09 , 2_2(363) -> 362 1154.25/297.09 , 2_2(369) -> 368 1154.25/297.09 , 2_2(370) -> 278 1154.25/297.09 , 2_2(377) -> 376 1154.25/297.09 , 2_2(379) -> 140 1154.25/297.09 , 2_2(386) -> 385 1154.25/297.09 , 2_2(388) -> 195 1154.25/297.09 , 2_2(395) -> 394 1154.25/297.09 , 2_2(397) -> 275 1154.25/297.09 , 2_2(404) -> 403 1154.25/297.09 , 2_2(406) -> 314 1154.25/297.09 , 2_2(413) -> 412 1154.25/297.09 , 2_2(417) -> 416 1154.25/297.09 , 2_2(419) -> 418 1154.25/297.09 , 2_2(425) -> 424 1154.25/297.09 , 2_2(427) -> 426 1154.25/297.09 , 2_2(433) -> 432 1154.25/297.09 , 2_2(435) -> 434 1154.25/297.09 , 2_2(441) -> 440 1154.25/297.09 , 2_2(443) -> 442 1154.25/297.09 , 2_2(449) -> 448 1154.25/297.09 , 2_2(451) -> 450 1154.25/297.09 , 2_2(477) -> 476 1154.25/297.09 , 2_2(491) -> 490 1154.25/297.09 , 2_2(505) -> 504 1154.25/297.09 , 2_2(512) -> 511 1154.25/297.09 , 2_2(525) -> 524 1154.25/297.09 , 2_2(531) -> 530 1154.25/297.09 , 2_2(532) -> 531 1154.25/297.09 , 2_2(533) -> 532 1154.25/297.09 , 2_2(539) -> 538 1154.25/297.09 , 2_2(547) -> 546 1154.25/297.09 , 2_2(552) -> 551 1154.25/297.09 , 2_2(556) -> 555 1154.25/297.09 , 3_0(1) -> 1 1154.25/297.09 , 3_1(1) -> 42 1154.25/297.09 , 3_1(2) -> 42 1154.25/297.09 , 3_1(3) -> 2 1154.25/297.09 , 3_1(12) -> 42 1154.25/297.09 , 3_1(17) -> 16 1154.25/297.09 , 3_1(25) -> 239 1154.25/297.09 , 3_1(26) -> 127 1154.25/297.09 , 3_1(27) -> 42 1154.25/297.09 , 3_1(28) -> 27 1154.25/297.09 , 3_1(33) -> 127 1154.25/297.09 , 3_1(34) -> 179 1154.25/297.09 , 3_1(42) -> 84 1154.25/297.09 , 3_1(43) -> 42 1154.25/297.09 , 3_1(45) -> 42 1154.25/297.09 , 3_1(51) -> 147 1154.25/297.09 , 3_1(52) -> 42 1154.25/297.09 , 3_1(53) -> 52 1154.25/297.09 , 3_1(55) -> 54 1154.25/297.09 , 3_1(58) -> 313 1154.25/297.09 , 3_1(77) -> 42 1154.25/297.09 , 3_1(82) -> 81 1154.25/297.09 , 3_1(83) -> 82 1154.25/297.09 , 3_1(105) -> 104 1154.25/297.09 , 3_1(106) -> 213 1154.25/297.09 , 3_1(121) -> 1 1154.25/297.09 , 3_1(121) -> 10 1154.25/297.09 , 3_1(121) -> 42 1154.25/297.09 , 3_1(121) -> 67 1154.25/297.09 , 3_1(121) -> 84 1154.25/297.09 , 3_1(121) -> 179 1154.25/297.09 , 3_1(121) -> 278 1154.25/297.09 , 3_1(121) -> 378 1154.25/297.09 , 3_1(121) -> 422 1154.25/297.09 , 3_1(129) -> 128 1154.25/297.09 , 3_1(135) -> 42 1154.25/297.09 , 3_1(136) -> 135 1154.25/297.09 , 3_1(138) -> 137 1154.25/297.09 , 3_1(139) -> 138 1154.25/297.09 , 3_1(140) -> 139 1154.25/297.09 , 3_1(142) -> 35 1154.25/297.09 , 3_1(144) -> 143 1154.25/297.09 , 3_1(150) -> 149 1154.25/297.09 , 3_1(163) -> 42 1154.25/297.09 , 3_1(168) -> 43 1154.25/297.09 , 3_1(170) -> 169 1154.25/297.09 , 3_1(180) -> 121 1154.25/297.09 , 3_1(185) -> 326 1154.25/297.09 , 3_1(188) -> 187 1154.25/297.09 , 3_1(197) -> 16 1154.25/297.09 , 3_1(202) -> 287 1154.25/297.09 , 3_1(203) -> 42 1154.25/297.09 , 3_1(210) -> 164 1154.25/297.09 , 3_1(230) -> 229 1154.25/297.09 , 3_1(235) -> 234 1154.25/297.09 , 3_1(238) -> 237 1154.25/297.09 , 3_1(254) -> 77 1154.25/297.09 , 3_1(258) -> 257 1154.25/297.09 , 3_1(262) -> 261 1154.25/297.09 , 3_1(263) -> 262 1154.25/297.09 , 3_1(264) -> 263 1154.25/297.09 , 3_1(268) -> 42 1154.25/297.09 , 3_1(280) -> 279 1154.25/297.09 , 3_1(289) -> 288 1154.25/297.09 , 3_1(290) -> 289 1154.25/297.09 , 3_1(294) -> 293 1154.25/297.09 , 3_1(295) -> 294 1154.25/297.09 , 3_1(297) -> 296 1154.25/297.09 , 3_1(298) -> 180 1154.25/297.09 , 3_1(314) -> 11 1154.25/297.09 , 3_1(317) -> 316 1154.25/297.09 , 3_1(327) -> 326 1154.25/297.09 , 3_1(331) -> 330 1154.25/297.09 , 3_1(357) -> 356 1154.25/297.09 , 3_2(1) -> 378 1154.25/297.09 , 3_2(2) -> 67 1154.25/297.09 , 3_2(9) -> 76 1154.25/297.09 , 3_2(12) -> 227 1154.25/297.09 , 3_2(34) -> 67 1154.25/297.09 , 3_2(43) -> 67 1154.25/297.09 , 3_2(45) -> 227 1154.25/297.09 , 3_2(49) -> 405 1154.25/297.09 , 3_2(52) -> 162 1154.25/297.09 , 3_2(60) -> 535 1154.25/297.09 , 3_2(61) -> 60 1154.25/297.09 , 3_2(63) -> 62 1154.25/297.09 , 3_2(67) -> 92 1154.25/297.09 , 3_2(70) -> 69 1154.25/297.09 , 3_2(72) -> 71 1154.25/297.09 , 3_2(76) -> 100 1154.25/297.09 , 3_2(77) -> 67 1154.25/297.09 , 3_2(90) -> 89 1154.25/297.09 , 3_2(91) -> 90 1154.25/297.09 , 3_2(98) -> 97 1154.25/297.09 , 3_2(99) -> 98 1154.25/297.09 , 3_2(106) -> 387 1154.25/297.09 , 3_2(111) -> 110 1154.25/297.09 , 3_2(118) -> 117 1154.25/297.09 , 3_2(154) -> 10 1154.25/297.09 , 3_2(154) -> 173 1154.25/297.09 , 3_2(157) -> 156 1154.25/297.09 , 3_2(163) -> 67 1154.25/297.09 , 3_2(197) -> 396 1154.25/297.09 , 3_2(203) -> 67 1154.25/297.09 , 3_2(214) -> 67 1154.25/297.09 , 3_2(242) -> 241 1154.25/297.09 , 3_2(245) -> 244 1154.25/297.09 , 3_2(247) -> 246 1154.25/297.09 , 3_2(268) -> 67 1154.25/297.09 , 3_2(277) -> 405 1154.25/297.09 , 3_2(316) -> 414 1154.25/297.09 , 3_2(329) -> 67 1154.25/297.09 , 3_2(348) -> 347 1154.25/297.09 , 3_2(367) -> 366 1154.25/297.09 , 3_2(372) -> 371 1154.25/297.09 , 3_2(374) -> 373 1154.25/297.09 , 3_2(378) -> 422 1154.25/297.09 , 3_2(381) -> 380 1154.25/297.09 , 3_2(383) -> 382 1154.25/297.09 , 3_2(387) -> 430 1154.25/297.09 , 3_2(390) -> 389 1154.25/297.09 , 3_2(392) -> 391 1154.25/297.09 , 3_2(396) -> 438 1154.25/297.09 , 3_2(399) -> 398 1154.25/297.09 , 3_2(401) -> 400 1154.25/297.09 , 3_2(405) -> 446 1154.25/297.09 , 3_2(408) -> 407 1154.25/297.09 , 3_2(410) -> 409 1154.25/297.09 , 3_2(414) -> 454 1154.25/297.09 , 3_2(420) -> 419 1154.25/297.09 , 3_2(421) -> 420 1154.25/297.09 , 3_2(428) -> 427 1154.25/297.09 , 3_2(429) -> 428 1154.25/297.09 , 3_2(436) -> 435 1154.25/297.09 , 3_2(437) -> 436 1154.25/297.09 , 3_2(444) -> 443 1154.25/297.09 , 3_2(445) -> 444 1154.25/297.09 , 3_2(452) -> 451 1154.25/297.09 , 3_2(453) -> 452 1154.25/297.09 , 3_2(480) -> 479 1154.25/297.09 , 3_2(494) -> 493 1154.25/297.09 , 3_2(508) -> 507 1154.25/297.09 , 3_2(515) -> 514 1154.25/297.09 , 3_2(520) -> 519 1154.25/297.09 , 3_2(522) -> 521 1154.25/297.09 , 3_2(526) -> 525 1154.25/297.09 , 3_2(527) -> 207 1154.25/297.09 , 3_2(530) -> 529 1154.25/297.09 , 3_2(538) -> 537 1154.25/297.09 , 3_2(541) -> 540 1154.25/297.09 , 3_2(543) -> 542 1154.25/297.09 , 3_2(546) -> 545 1154.25/297.09 , 3_2(549) -> 548 1154.25/297.09 , 3_2(551) -> 550 1154.25/297.09 , 3_2(553) -> 67 1154.25/297.09 , 3_2(555) -> 554 1154.25/297.09 , 3_2(558) -> 557 1154.25/297.09 , 3_2(560) -> 559 1154.25/297.09 , 4_0(1) -> 1 1154.25/297.09 , 4_1(1) -> 26 1154.25/297.09 , 4_1(2) -> 26 1154.25/297.09 , 4_1(6) -> 5 1154.25/297.09 , 4_1(10) -> 9 1154.25/297.09 , 4_1(12) -> 11 1154.25/297.09 , 4_1(15) -> 14 1154.25/297.09 , 4_1(18) -> 17 1154.25/297.09 , 4_1(19) -> 197 1154.25/297.09 , 4_1(20) -> 3 1154.25/297.09 , 4_1(26) -> 346 1154.25/297.09 , 4_1(29) -> 28 1154.25/297.09 , 4_1(30) -> 29 1154.25/297.09 , 4_1(34) -> 33 1154.25/297.09 , 4_1(35) -> 2 1154.25/297.09 , 4_1(40) -> 39 1154.25/297.09 , 4_1(41) -> 40 1154.25/297.09 , 4_1(42) -> 41 1154.25/297.09 , 4_1(43) -> 26 1154.25/297.09 , 4_1(45) -> 44 1154.25/297.09 , 4_1(49) -> 48 1154.25/297.09 , 4_1(50) -> 265 1154.25/297.09 , 4_1(51) -> 302 1154.25/297.09 , 4_1(54) -> 53 1154.25/297.09 , 4_1(58) -> 153 1154.25/297.09 , 4_1(77) -> 1 1154.25/297.09 , 4_1(77) -> 10 1154.25/297.09 , 4_1(77) -> 19 1154.25/297.09 , 4_1(77) -> 25 1154.25/297.09 , 4_1(77) -> 274 1154.25/297.09 , 4_1(77) -> 543 1154.25/297.09 , 4_1(78) -> 77 1154.25/297.09 , 4_1(80) -> 79 1154.25/297.09 , 4_1(101) -> 78 1154.25/297.09 , 4_1(106) -> 105 1154.25/297.09 , 4_1(126) -> 125 1154.25/297.09 , 4_1(127) -> 167 1154.25/297.09 , 4_1(130) -> 129 1154.25/297.09 , 4_1(134) -> 145 1154.25/297.09 , 4_1(145) -> 144 1154.25/297.09 , 4_1(146) -> 145 1154.25/297.09 , 4_1(147) -> 328 1154.25/297.09 , 4_1(153) -> 251 1154.25/297.09 , 4_1(167) -> 166 1154.25/297.09 , 4_1(172) -> 171 1154.25/297.09 , 4_1(183) -> 182 1154.25/297.09 , 4_1(189) -> 188 1154.25/297.09 , 4_1(193) -> 192 1154.25/297.09 , 4_1(197) -> 233 1154.25/297.09 , 4_1(202) -> 218 1154.25/297.09 , 4_1(203) -> 26 1154.25/297.09 , 4_1(206) -> 205 1154.25/297.09 , 4_1(207) -> 206 1154.25/297.09 , 4_1(212) -> 211 1154.25/297.09 , 4_1(213) -> 212 1154.25/297.09 , 4_1(216) -> 215 1154.25/297.09 , 4_1(231) -> 230 1154.25/297.09 , 4_1(232) -> 231 1154.25/297.09 , 4_1(237) -> 236 1154.25/297.09 , 4_1(249) -> 203 1154.25/297.09 , 4_1(252) -> 251 1154.25/297.09 , 4_1(253) -> 252 1154.25/297.09 , 4_1(259) -> 258 1154.25/297.09 , 4_1(266) -> 265 1154.25/297.09 , 4_1(268) -> 43 1154.25/297.09 , 4_1(274) -> 171 1154.25/297.09 , 4_1(279) -> 122 1154.25/297.09 , 4_1(286) -> 285 1154.25/297.09 , 4_1(302) -> 301 1154.25/297.09 , 4_1(303) -> 302 1154.25/297.09 , 4_1(313) -> 312 1154.25/297.09 , 4_1(321) -> 320 1154.25/297.09 , 4_1(329) -> 26 1154.25/297.09 , 4_1(333) -> 332 1154.25/297.09 , 4_1(334) -> 333 1154.25/297.09 , 4_1(336) -> 335 1154.25/297.09 , 4_1(337) -> 336 1154.25/297.09 , 4_1(343) -> 342 1154.25/297.09 , 4_1(344) -> 343 1154.25/297.09 , 4_1(358) -> 357 1154.25/297.09 , 4_2(1) -> 113 1154.25/297.09 , 4_2(2) -> 113 1154.25/297.09 , 4_2(9) -> 120 1154.25/297.09 , 4_2(34) -> 113 1154.25/297.09 , 4_2(41) -> 248 1154.25/297.09 , 4_2(43) -> 113 1154.25/297.09 , 4_2(47) -> 355 1154.25/297.09 , 4_2(49) -> 510 1154.25/297.09 , 4_2(62) -> 61 1154.25/297.09 , 4_2(71) -> 70 1154.25/297.09 , 4_2(77) -> 113 1154.25/297.09 , 4_2(85) -> 10 1154.25/297.09 , 4_2(85) -> 208 1154.25/297.09 , 4_2(85) -> 275 1154.25/297.09 , 4_2(85) -> 278 1154.25/297.09 , 4_2(86) -> 85 1154.25/297.09 , 4_2(88) -> 87 1154.25/297.09 , 4_2(93) -> 7 1154.25/297.09 , 4_2(94) -> 93 1154.25/297.09 , 4_2(96) -> 95 1154.25/297.09 , 4_2(106) -> 482 1154.25/297.09 , 4_2(107) -> 86 1154.25/297.09 , 4_2(112) -> 111 1154.25/297.09 , 4_2(114) -> 94 1154.25/297.09 , 4_2(119) -> 118 1154.25/297.09 , 4_2(161) -> 160 1154.25/297.09 , 4_2(163) -> 113 1154.25/297.09 , 4_2(197) -> 496 1154.25/297.09 , 4_2(203) -> 113 1154.25/297.09 , 4_2(214) -> 113 1154.25/297.09 , 4_2(222) -> 221 1154.25/297.09 , 4_2(225) -> 224 1154.25/297.09 , 4_2(227) -> 226 1154.25/297.09 , 4_2(244) -> 243 1154.25/297.09 , 4_2(268) -> 113 1154.25/297.09 , 4_2(277) -> 510 1154.25/297.09 , 4_2(310) -> 552 1154.25/297.09 , 4_2(316) -> 517 1154.25/297.09 , 4_2(329) -> 355 1154.25/297.09 , 4_2(351) -> 350 1154.25/297.09 , 4_2(352) -> 351 1154.25/297.09 , 4_2(355) -> 354 1154.25/297.09 , 4_2(362) -> 361 1154.25/297.09 , 4_2(365) -> 364 1154.25/297.09 , 4_2(368) -> 367 1154.25/297.09 , 4_2(373) -> 372 1154.25/297.09 , 4_2(382) -> 381 1154.25/297.09 , 4_2(391) -> 390 1154.25/297.09 , 4_2(400) -> 399 1154.25/297.09 , 4_2(409) -> 408 1154.25/297.09 , 4_2(415) -> 278 1154.25/297.09 , 4_2(416) -> 415 1154.25/297.09 , 4_2(418) -> 417 1154.25/297.09 , 4_2(423) -> 140 1154.25/297.09 , 4_2(424) -> 423 1154.25/297.09 , 4_2(426) -> 425 1154.25/297.09 , 4_2(431) -> 195 1154.25/297.09 , 4_2(432) -> 431 1154.25/297.09 , 4_2(434) -> 433 1154.25/297.09 , 4_2(439) -> 275 1154.25/297.09 , 4_2(440) -> 439 1154.25/297.09 , 4_2(442) -> 441 1154.25/297.09 , 4_2(447) -> 314 1154.25/297.09 , 4_2(448) -> 447 1154.25/297.09 , 4_2(450) -> 449 1154.25/297.09 , 4_2(476) -> 424 1154.25/297.09 , 4_2(481) -> 480 1154.25/297.09 , 4_2(490) -> 432 1154.25/297.09 , 4_2(495) -> 494 1154.25/297.09 , 4_2(504) -> 440 1154.25/297.09 , 4_2(509) -> 508 1154.25/297.09 , 4_2(511) -> 448 1154.25/297.09 , 4_2(516) -> 515 1154.25/297.09 , 4_2(519) -> 518 1154.25/297.09 , 4_2(523) -> 522 1154.25/297.09 , 4_2(524) -> 523 1154.25/297.09 , 4_2(534) -> 533 1154.25/297.09 , 4_2(540) -> 539 1154.25/297.09 , 4_2(548) -> 547 1154.25/297.09 , 4_2(553) -> 113 1154.25/297.09 , 4_2(557) -> 556 1154.25/297.09 , 5_0(1) -> 1 1154.25/297.09 , 5_1(1) -> 51 1154.25/297.09 , 5_1(11) -> 1 1154.25/297.09 , 5_1(11) -> 10 1154.25/297.09 , 5_1(11) -> 42 1154.25/297.09 , 5_1(11) -> 51 1154.25/297.09 , 5_1(11) -> 147 1154.25/297.09 , 5_1(11) -> 260 1154.25/297.09 , 5_1(11) -> 278 1154.25/297.09 , 5_1(11) -> 303 1154.25/297.09 , 5_1(11) -> 334 1154.25/297.09 , 5_1(11) -> 340 1154.25/297.09 , 5_1(11) -> 378 1154.25/297.09 , 5_1(19) -> 340 1154.25/297.09 , 5_1(24) -> 23 1154.25/297.09 , 5_1(25) -> 24 1154.25/297.09 , 5_1(26) -> 303 1154.25/297.09 , 5_1(31) -> 30 1154.25/297.09 , 5_1(34) -> 260 1154.25/297.09 , 5_1(36) -> 35 1154.25/297.09 , 5_1(37) -> 36 1154.25/297.09 , 5_1(38) -> 37 1154.25/297.09 , 5_1(44) -> 43 1154.25/297.09 , 5_1(46) -> 45 1154.25/297.09 , 5_1(51) -> 267 1154.25/297.09 , 5_1(84) -> 334 1154.25/297.09 , 5_1(123) -> 122 1154.25/297.09 , 5_1(127) -> 319 1154.25/297.09 , 5_1(128) -> 11 1154.25/297.09 , 5_1(133) -> 132 1154.25/297.09 , 5_1(135) -> 340 1154.25/297.09 , 5_1(166) -> 165 1154.25/297.09 , 5_1(174) -> 148 1154.25/297.09 , 5_1(186) -> 77 1154.25/297.09 , 5_1(187) -> 186 1154.25/297.09 , 5_1(192) -> 191 1154.25/297.09 , 5_1(202) -> 201 1154.25/297.09 , 5_1(211) -> 210 1154.25/297.09 , 5_1(215) -> 214 1154.25/297.09 , 5_1(233) -> 232 1154.25/297.09 , 5_1(234) -> 2 1154.25/297.09 , 5_1(265) -> 264 1154.25/297.09 , 5_1(273) -> 272 1154.25/297.09 , 5_1(274) -> 273 1154.25/297.09 , 5_1(285) -> 284 1154.25/297.09 , 5_1(301) -> 300 1154.25/297.09 , 5_1(307) -> 306 1154.25/297.09 , 5_1(309) -> 308 1154.25/297.09 , 5_1(323) -> 322 1154.25/297.09 , 5_1(340) -> 339 1154.25/297.09 , 5_1(342) -> 341 1154.25/297.09 , 5_1(359) -> 358 1154.25/297.09 , 5_2(44) -> 526 1154.25/297.09 , 5_2(221) -> 220 1154.25/297.09 , 5_2(241) -> 240 1154.25/297.09 , 5_2(347) -> 334 1154.25/297.09 , 5_2(350) -> 349 1154.25/297.09 , 5_2(361) -> 207 1154.25/297.09 , 5_2(537) -> 536 1154.25/297.09 , 5_2(545) -> 544 1154.25/297.09 , 5_2(554) -> 553 } 1154.25/297.09 1154.25/297.09 Hurray, we answered YES(?,O(n^1)) 1155.35/297.92 EOF