YES(?,O(n^1))
15.76/4.25	YES(?,O(n^1))
15.76/4.26	
15.76/4.26	Problem:
15.76/4.26	 b(a(a(a(b(a(a(x1))))))) -> a(a(a(b(b(a(a(a(b(x1)))))))))
15.76/4.26	
15.76/4.26	Proof:
15.76/4.26	 Bounds Processor:
15.76/4.26	  bound: 5
15.76/4.26	  enrichment: match
15.76/4.26	  automaton:
15.76/4.26	   final states: {3}
15.76/4.26	   transitions:
15.76/4.26	    b3(656) -> 657*
15.76/4.26	    b3(434) -> 435*
15.76/4.26	    b3(404) -> 405*
15.76/4.26	    b3(344) -> 345*
15.76/4.26	    b3(319) -> 320*
15.76/4.26	    b3(516) -> 517*
15.76/4.26	    b3(314) -> 315*
15.76/4.26	    b3(486) -> 487*
15.76/4.26	    b3(254) -> 255*
15.76/4.26	    b3(234) -> 235*
15.76/4.26	    b3(224) -> 225*
15.76/4.26	    b3(386) -> 387*
15.76/4.26	    b3(376) -> 377*
15.76/4.26	    b3(568) -> 569*
15.76/4.26	    b3(154) -> 155*
15.76/4.26	    b3(351) -> 352*
15.76/4.26	    b3(346) -> 347*
15.76/4.26	    b3(523) -> 524*
15.76/4.26	    b3(518) -> 519*
15.76/4.26	    b3(296) -> 297*
15.76/4.26	    b3(615) -> 616*
15.76/4.26	    b3(610) -> 611*
15.76/4.26	    b3(176) -> 177*
15.76/4.26	    b3(171) -> 172*
15.76/4.26	    b3(166) -> 167*
15.76/4.26	    b3(318) -> 319*
15.76/4.26	    b3(440) -> 441*
15.76/4.26	    b3(435) -> 436*
15.76/4.26	    b3(430) -> 431*
15.76/4.26	    b3(400) -> 401*
15.76/4.26	    b3(350) -> 351*
15.76/4.26	    b3(522) -> 523*
15.76/4.26	    b3(290) -> 291*
15.76/4.26	    b3(462) -> 463*
15.76/4.26	    b3(255) -> 256*
15.76/4.26	    b3(654) -> 655*
15.76/4.26	    b3(250) -> 251*
15.76/4.26	    b3(235) -> 236*
15.76/4.26	    b3(230) -> 231*
15.76/4.26	    b3(225) -> 226*
15.76/4.26	    b3(220) -> 221*
15.76/4.26	    b3(614) -> 615*
15.76/4.26	    b3(387) -> 388*
15.76/4.26	    b3(382) -> 383*
15.76/4.26	    b3(170) -> 171*
15.76/4.26	    b3(569) -> 570*
15.76/4.26	    b3(564) -> 565*
15.76/4.26	    b3(160) -> 161*
15.76/4.26	    b3(155) -> 156*
15.76/4.26	    b3(150) -> 151*
15.76/4.26	    a4(676) -> 677*
15.76/4.26	    a4(671) -> 672*
15.76/4.26	    a4(636) -> 637*
15.76/4.26	    a4(631) -> 632*
15.76/4.26	    a4(414) -> 415*
15.76/4.26	    a4(409) -> 410*
15.76/4.26	    a4(606) -> 607*
15.76/4.26	    a4(601) -> 602*
15.76/4.26	    a4(561) -> 562*
15.76/4.26	    a4(556) -> 557*
15.76/4.26	    a4(511) -> 512*
15.76/4.26	    a4(506) -> 507*
15.76/4.26	    a4(496) -> 497*
15.76/4.26	    a4(491) -> 492*
15.76/4.26	    a4(678) -> 679*
15.76/4.26	    a4(673) -> 674*
15.76/4.26	    a4(638) -> 639*
15.76/4.26	    a4(633) -> 634*
15.76/4.26	    a4(416) -> 417*
15.76/4.26	    a4(411) -> 412*
15.76/4.26	    a4(608) -> 609*
15.76/4.26	    a4(603) -> 604*
15.76/4.26	    a4(341) -> 342*
15.76/4.26	    a4(336) -> 337*
15.76/4.26	    a4(286) -> 287*
15.76/4.26	    a4(281) -> 282*
15.76/4.26	    a4(560) -> 561*
15.76/4.26	    a4(555) -> 556*
15.76/4.26	    a4(510) -> 511*
15.76/4.26	    a4(505) -> 506*
15.76/4.26	    a4(495) -> 496*
15.76/4.26	    a4(490) -> 491*
15.76/4.26	    a4(288) -> 289*
15.76/4.26	    a4(283) -> 284*
15.76/4.26	    a4(677) -> 678*
15.76/4.26	    a4(672) -> 673*
15.76/4.26	    a4(637) -> 638*
15.76/4.26	    a4(632) -> 633*
15.76/4.26	    a4(415) -> 416*
15.76/4.26	    a4(410) -> 411*
15.76/4.26	    a4(607) -> 608*
15.76/4.26	    a4(602) -> 603*
15.76/4.26	    a4(562) -> 563*
15.76/4.26	    a4(557) -> 558*
15.76/4.26	    a4(340) -> 341*
15.76/4.26	    a4(335) -> 336*
15.76/4.26	    a4(512) -> 513*
15.76/4.26	    a4(507) -> 508*
15.76/4.26	    a4(342) -> 343*
15.76/4.26	    a4(337) -> 338*
15.76/4.26	    a4(494) -> 495*
15.76/4.26	    a4(489) -> 490*
15.76/4.26	    a4(287) -> 288*
15.76/4.26	    a4(282) -> 283*
15.76/4.26	    b4(464) -> 465*
15.76/4.26	    b4(339) -> 340*
15.76/4.26	    b4(334) -> 335*
15.76/4.26	    b4(284) -> 285*
15.76/4.26	    b4(578) -> 579*
15.76/4.26	    b4(558) -> 559*
15.76/4.26	    b4(710) -> 711*
15.76/4.26	    b4(508) -> 509*
15.76/4.26	    b4(493) -> 494*
15.76/4.26	    b4(488) -> 489*
15.76/4.26	    b4(675) -> 676*
15.76/4.26	    b4(670) -> 671*
15.76/4.26	    b4(640) -> 641*
15.76/4.26	    b4(635) -> 636*
15.76/4.26	    b4(630) -> 631*
15.76/4.26	    b4(413) -> 414*
15.76/4.26	    b4(408) -> 409*
15.76/4.26	    b4(605) -> 606*
15.76/4.26	    b4(600) -> 601*
15.76/4.26	    b4(540) -> 541*
15.76/4.26	    b4(338) -> 339*
15.76/4.26	    b4(502) -> 503*
15.76/4.26	    b4(694) -> 695*
15.76/4.26	    b4(492) -> 493*
15.76/4.26	    b4(285) -> 286*
15.76/4.26	    b4(280) -> 281*
15.76/4.26	    b4(674) -> 675*
15.76/4.26	    b4(634) -> 635*
15.76/4.26	    b4(412) -> 413*
15.76/4.26	    b4(604) -> 605*
15.76/4.26	    b4(594) -> 595*
15.76/4.26	    b4(559) -> 560*
15.76/4.26	    b4(554) -> 555*
15.76/4.26	    b4(509) -> 510*
15.76/4.26	    b4(504) -> 505*
15.76/4.26	    b4(696) -> 697*
15.76/4.26	    b0(3) -> 3*
15.76/4.26	    a5(681) -> 682*
15.76/4.26	    a5(591) -> 592*
15.76/4.26	    a5(586) -> 587*
15.76/4.26	    a5(688) -> 689*
15.76/4.26	    a5(683) -> 684*
15.76/4.26	    a5(590) -> 591*
15.76/4.26	    a5(585) -> 586*
15.76/4.26	    a5(687) -> 688*
15.76/4.26	    a5(682) -> 683*
15.76/4.26	    a5(592) -> 593*
15.76/4.26	    a5(587) -> 588*
15.76/4.26	    a5(686) -> 687*
15.76/4.26	    a0(3) -> 3*
15.76/4.26	    b5(588) -> 589*
15.76/4.26	    b5(685) -> 686*
15.76/4.26	    b5(680) -> 681*
15.76/4.26	    b5(684) -> 685*
15.76/4.26	    b5(589) -> 590*
15.76/4.26	    b5(584) -> 585*
15.76/4.26	    a1(20) -> 21*
15.76/4.26	    a1(15) -> 16*
15.76/4.26	    a1(52) -> 53*
15.76/4.26	    a1(47) -> 48*
15.76/4.26	    a1(22) -> 23*
15.76/4.26	    a1(17) -> 18*
15.76/4.26	    a1(54) -> 55*
15.76/4.26	    a1(49) -> 50*
15.76/4.26	    a1(21) -> 22*
15.76/4.26	    a1(16) -> 17*
15.76/4.26	    a1(53) -> 54*
15.76/4.26	    a1(48) -> 49*
15.76/4.26	    b1(50) -> 51*
15.76/4.26	    b1(92) -> 93*
15.76/4.26	    b1(144) -> 145*
15.76/4.26	    b1(19) -> 20*
15.76/4.26	    b1(14) -> 15*
15.76/4.26	    b1(206) -> 207*
15.76/4.26	    b1(51) -> 52*
15.76/4.26	    b1(46) -> 47*
15.76/4.26	    b1(88) -> 89*
15.76/4.26	    b1(58) -> 59*
15.76/4.26	    b1(18) -> 19*
15.76/4.26	    b1(90) -> 91*
15.76/4.26	    a2(75) -> 76*
15.76/4.26	    a2(30) -> 31*
15.76/4.26	    a2(25) -> 26*
15.76/4.26	    a2(192) -> 193*
15.76/4.26	    a2(187) -> 188*
15.76/4.26	    a2(127) -> 128*
15.76/4.26	    a2(122) -> 123*
15.76/4.26	    a2(32) -> 33*
15.76/4.26	    a2(27) -> 28*
15.76/4.26	    a2(104) -> 105*
15.76/4.26	    a2(99) -> 100*
15.76/4.26	    a2(79) -> 80*
15.76/4.26	    a2(74) -> 75*
15.76/4.26	    a2(191) -> 192*
15.76/4.26	    a2(186) -> 187*
15.76/4.26	    a2(126) -> 127*
15.76/4.26	    a2(121) -> 122*
15.76/4.26	    a2(106) -> 107*
15.76/4.26	    a2(101) -> 102*
15.76/4.26	    a2(31) -> 32*
15.76/4.26	    a2(26) -> 27*
15.76/4.26	    a2(128) -> 129*
15.76/4.26	    a2(123) -> 124*
15.76/4.26	    a2(78) -> 79*
15.76/4.26	    a2(73) -> 74*
15.76/4.26	    a2(190) -> 191*
15.76/4.26	    a2(185) -> 186*
15.76/4.26	    a2(105) -> 106*
15.76/4.26	    a2(100) -> 101*
15.76/4.26	    a2(80) -> 81*
15.76/4.26	    b2(182) -> 183*
15.76/4.26	    b2(142) -> 143*
15.76/4.26	    b2(102) -> 103*
15.76/4.26	    b2(77) -> 78*
15.76/4.26	    b2(274) -> 275*
15.76/4.26	    b2(72) -> 73*
15.76/4.26	    b2(189) -> 190*
15.76/4.26	    b2(184) -> 185*
15.76/4.26	    b2(124) -> 125*
15.76/4.26	    b2(29) -> 30*
15.76/4.26	    b2(24) -> 25*
15.76/4.26	    b2(398) -> 399*
15.76/4.26	    b2(146) -> 147*
15.76/4.26	    b2(298) -> 299*
15.76/4.26	    b2(86) -> 87*
15.76/4.26	    b2(76) -> 77*
15.76/4.26	    b2(188) -> 189*
15.76/4.26	    b2(103) -> 104*
15.76/4.26	    b2(98) -> 99*
15.76/4.26	    b2(260) -> 261*
15.76/4.26	    b2(28) -> 29*
15.76/4.26	    b2(392) -> 393*
15.76/4.26	    b2(130) -> 131*
15.76/4.26	    b2(125) -> 126*
15.76/4.26	    b2(120) -> 121*
15.76/4.26	    b2(312) -> 313*
15.76/4.26	    a3(257) -> 258*
15.76/4.26	    a3(252) -> 253*
15.76/4.26	    a3(237) -> 238*
15.76/4.26	    a3(232) -> 233*
15.76/4.26	    a3(227) -> 228*
15.76/4.26	    a3(222) -> 223*
15.76/4.26	    a3(616) -> 617*
15.76/4.26	    a3(611) -> 612*
15.76/4.26	    a3(389) -> 390*
15.76/4.26	    a3(384) -> 385*
15.76/4.26	    a3(172) -> 173*
15.76/4.26	    a3(571) -> 572*
15.76/4.26	    a3(167) -> 168*
15.76/4.26	    a3(566) -> 567*
15.76/4.26	    a3(157) -> 158*
15.76/4.26	    a3(354) -> 355*
15.76/4.26	    a3(152) -> 153*
15.76/4.26	    a3(349) -> 350*
15.76/4.26	    a3(526) -> 527*
15.76/4.26	    a3(521) -> 522*
15.76/4.26	    a3(436) -> 437*
15.76/4.26	    a3(431) -> 432*
15.76/4.26	    a3(618) -> 619*
15.76/4.26	    a3(613) -> 614*
15.76/4.26	    a3(174) -> 175*
15.76/4.26	    a3(169) -> 170*
15.76/4.26	    a3(321) -> 322*
15.76/4.26	    a3(316) -> 317*
15.76/4.26	    a3(256) -> 257*
15.76/4.26	    a3(251) -> 252*
15.76/4.26	    a3(438) -> 439*
15.76/4.26	    a3(236) -> 237*
15.76/4.26	    a3(433) -> 434*
15.76/4.26	    a3(231) -> 232*
15.76/4.26	    a3(226) -> 227*
15.76/4.26	    a3(221) -> 222*
15.76/4.26	    a3(388) -> 389*
15.76/4.26	    a3(383) -> 384*
15.76/4.26	    a3(570) -> 571*
15.76/4.26	    a3(565) -> 566*
15.76/4.26	    a3(156) -> 157*
15.76/4.26	    a3(353) -> 354*
15.76/4.26	    a3(151) -> 152*
15.76/4.26	    a3(348) -> 349*
15.76/4.26	    a3(525) -> 526*
15.76/4.26	    a3(520) -> 521*
15.76/4.26	    a3(258) -> 259*
15.76/4.26	    a3(253) -> 254*
15.76/4.26	    a3(238) -> 239*
15.76/4.26	    a3(233) -> 234*
15.76/4.26	    a3(228) -> 229*
15.76/4.26	    a3(223) -> 224*
15.76/4.26	    a3(617) -> 618*
15.76/4.26	    a3(612) -> 613*
15.76/4.26	    a3(390) -> 391*
15.76/4.26	    a3(385) -> 386*
15.76/4.26	    a3(173) -> 174*
15.76/4.26	    a3(572) -> 573*
15.76/4.26	    a3(168) -> 169*
15.76/4.26	    a3(567) -> 568*
15.76/4.26	    a3(158) -> 159*
15.76/4.26	    a3(153) -> 154*
15.76/4.26	    a3(320) -> 321*
15.76/4.26	    a3(315) -> 316*
15.76/4.26	    a3(437) -> 438*
15.76/4.26	    a3(432) -> 433*
15.76/4.26	    a3(352) -> 353*
15.76/4.26	    a3(347) -> 348*
15.76/4.26	    a3(524) -> 525*
15.76/4.26	    a3(322) -> 323*
15.76/4.26	    a3(519) -> 520*
15.76/4.26	    a3(317) -> 318*
15.76/4.26	    3 -> 14*
15.76/4.26	    20 -> 98*
15.76/4.26	    21 -> 58,24
15.76/4.26	    22 -> 46*
15.76/4.26	    23 -> 15,19,3
15.76/4.26	    30 -> 176*
15.76/4.26	    31 -> 150,90,72
15.76/4.26	    32 -> 120*
15.76/4.26	    33 -> 15,20,19
15.76/4.26	    52 -> 146*
15.76/4.26	    53 -> 92,86
15.76/4.26	    54 -> 88*
15.76/4.26	    55 -> 15,3,14,19
15.76/4.26	    59 -> 15*
15.76/4.26	    78 -> 166*
15.76/4.26	    79 -> 160*
15.76/4.26	    80 -> 130*
15.76/4.26	    81 -> 15,20
15.76/4.26	    87 -> 25*
15.76/4.26	    89 -> 15*
15.76/4.26	    91 -> 15*
15.76/4.26	    93 -> 15*
15.76/4.26	    105 -> 144,142
15.76/4.26	    107 -> 51*
15.76/4.26	    127 -> 220,206,182
15.76/4.26	    129 -> 19,29
15.76/4.26	    131 -> 121*
15.76/4.26	    143 -> 25*
15.76/4.26	    145 -> 15*
15.76/4.26	    147 -> 25*
15.76/4.26	    157 -> 184*
15.76/4.26	    159 -> 103*
15.76/4.26	    161 -> 151*
15.76/4.26	    173 -> 274,230
15.76/4.26	    175 -> 125*
15.76/4.26	    177 -> 167*
15.76/4.26	    183 -> 25*
15.76/4.26	    190 -> 290*
15.76/4.26	    191 -> 250*
15.76/4.26	    192 -> 260*
15.76/4.26	    193 -> 52,146
15.76/4.26	    207 -> 15*
15.76/4.26	    226 -> 488,462
15.76/4.26	    228 -> 404,392
15.76/4.26	    229 -> 104,99
15.76/4.26	    236 -> 376,334
15.76/4.26	    237 -> 280*
15.76/4.26	    238 -> 314,312
15.76/4.26	    239 -> 30,176
15.76/4.26	    257 -> 298,296
15.76/4.26	    259 -> 225,29
15.76/4.26	    261 -> 121*
15.76/4.26	    275 -> 25*
15.76/4.26	    287 -> 346*
15.76/4.26	    289 -> 171*
15.76/4.26	    291 -> 167*
15.76/4.26	    297 -> 221*
15.76/4.26	    299 -> 25*
15.76/4.26	    313 -> 25*
15.76/4.26	    321 -> 344*
15.76/4.26	    323 -> 155,77
15.76/4.26	    341 -> 408,382
15.76/4.26	    343 -> 319*
15.76/4.26	    345 -> 221*
15.76/4.26	    352 -> 502,440
15.76/4.26	    354 -> 400,398
15.76/4.26	    355 -> 126*
15.76/4.26	    377 -> 251*
15.76/4.26	    388 -> 540*
15.76/4.26	    389 -> 464*
15.76/4.26	    390 -> 486*
15.76/4.26	    391 -> 78,166
15.76/4.26	    393 -> 25*
15.76/4.26	    399 -> 25*
15.76/4.26	    401 -> 251*
15.76/4.26	    405 -> 251*
15.76/4.26	    414 -> 554*
15.76/4.26	    416 -> 430*
15.76/4.26	    417 -> 156*
15.76/4.26	    437 -> 518*
15.76/4.26	    439 -> 189*
15.76/4.26	    441 -> 251*
15.76/4.26	    463 -> 251*
15.76/4.26	    465 -> 281*
15.76/4.26	    487 -> 315*
15.76/4.26	    495 -> 516,504
15.76/4.26	    497 -> 255*
15.76/4.26	    503 -> 489*
15.76/4.26	    511 -> 584,578
15.76/4.26	    513 -> 226*
15.76/4.26	    517 -> 231*
15.76/4.26	    527 -> 147,25
15.76/4.26	    541 -> 335*
15.76/4.26	    561 -> 564*
15.76/4.26	    563 -> 435*
15.76/4.26	    570 -> 670*
15.76/4.26	    571 -> 594*
15.76/4.26	    572 -> 610*
15.76/4.26	    573 -> 190,290
15.76/4.26	    579 -> 489*
15.76/4.26	    591 -> 600*
15.76/4.26	    593 -> 493*
15.76/4.26	    595 -> 281*
15.76/4.26	    606 -> 694,680
15.76/4.26	    608 -> 656,630
15.76/4.26	    609 -> 256*
15.76/4.26	    617 -> 654,640
15.76/4.26	    619 -> 255*
15.76/4.26	    639 -> 225*
15.76/4.26	    641 -> 505*
15.76/4.26	    655 -> 231*
15.76/4.26	    657 -> 251*
15.76/4.26	    677 -> 696*
15.76/4.26	    679 -> 615*
15.76/4.26	    687 -> 710*
15.76/4.26	    689 -> 635*
15.76/4.26	    695 -> 489*
15.76/4.26	    697 -> 601*
15.76/4.26	    711 -> 505*
15.76/4.26	  problem:
15.76/4.26	   
15.76/4.26	  Qed
15.76/4.26	EOF