YES(?,O(n^1))
8.79/2.50	YES(?,O(n^1))
9.23/2.50	
9.23/2.50	Problem:
9.23/2.50	 a(a(b(b(x1)))) -> b(b(b(a(a(a(a(a(x1))))))))
9.23/2.50	
9.23/2.50	Proof:
9.23/2.50	 Complexity Transformation Processor:
9.23/2.50	  strict:
9.23/2.50	   a(a(b(b(x1)))) -> b(b(b(a(a(a(a(a(x1))))))))
9.23/2.50	  weak:
9.23/2.50	   
9.23/2.50	  Bounds Processor:
9.23/2.50	   bound: 6
9.23/2.50	   enrichment: match
9.23/2.50	   automaton:
9.23/2.50	    final states: {2,1}
9.23/2.50	    transitions:
9.23/2.50	     a3(217) -> 218*
9.23/2.50	     a3(182) -> 183*
9.23/2.50	     a3(142) -> 143*
9.23/2.50	     a3(122) -> 123*
9.23/2.50	     a3(97) -> 98*
9.23/2.50	     a3(219) -> 220*
9.23/2.50	     a3(179) -> 180*
9.23/2.50	     a3(144) -> 145*
9.23/2.50	     a3(129) -> 130*
9.23/2.50	     a3(124) -> 125*
9.23/2.50	     a3(94) -> 95*
9.23/2.50	     a3(216) -> 217*
9.23/2.50	     a3(181) -> 182*
9.23/2.50	     a3(146) -> 147*
9.23/2.50	     a3(121) -> 122*
9.23/2.50	     a3(116) -> 117*
9.23/2.50	     a3(96) -> 97*
9.23/2.50	     a3(218) -> 219*
9.23/2.50	     a3(178) -> 179*
9.23/2.50	     a3(143) -> 144*
9.23/2.50	     a3(123) -> 124*
9.23/2.50	     a3(98) -> 99*
9.23/2.50	     a3(220) -> 221*
9.23/2.50	     a3(180) -> 181*
9.23/2.50	     a3(145) -> 146*
9.23/2.50	     a3(120) -> 121*
9.23/2.50	     a3(95) -> 96*
9.23/2.50	     b4(212) -> 213*
9.23/2.50	     b4(192) -> 193*
9.23/2.50	     b4(167) -> 168*
9.23/2.50	     b4(304) -> 305*
9.23/2.50	     b4(249) -> 250*
9.23/2.50	     b4(239) -> 240*
9.23/2.50	     b4(214) -> 215*
9.23/2.50	     b4(194) -> 195*
9.23/2.50	     b4(311) -> 312*
9.23/2.50	     b4(241) -> 242*
9.23/2.50	     b4(166) -> 167*
9.23/2.50	     b4(313) -> 314*
9.23/2.50	     b4(303) -> 304*
9.23/2.50	     b4(248) -> 249*
9.23/2.50	     b4(213) -> 214*
9.23/2.50	     b4(193) -> 194*
9.23/2.50	     b4(250) -> 251*
9.23/2.50	     b4(240) -> 241*
9.23/2.50	     b4(165) -> 166*
9.23/2.50	     b4(312) -> 313*
9.23/2.50	     b4(302) -> 303*
9.23/2.50	     a4(247) -> 248*
9.23/2.50	     a4(237) -> 238*
9.23/2.50	     a4(207) -> 208*
9.23/2.50	     a4(187) -> 188*
9.23/2.50	     a4(162) -> 163*
9.23/2.50	     a4(309) -> 310*
9.23/2.50	     a4(299) -> 300*
9.23/2.50	     a4(244) -> 245*
9.23/2.50	     a4(234) -> 235*
9.23/2.50	     a4(209) -> 210*
9.23/2.50	     a4(189) -> 190*
9.23/2.50	     a4(164) -> 165*
9.23/2.50	     a4(306) -> 307*
9.23/2.50	     a4(301) -> 302*
9.23/2.50	     a4(246) -> 247*
9.23/2.50	     a4(236) -> 237*
9.23/2.50	     a4(211) -> 212*
9.23/2.50	     a4(191) -> 192*
9.23/2.50	     a4(161) -> 162*
9.23/2.50	     a4(308) -> 309*
9.23/2.50	     a4(298) -> 299*
9.23/2.50	     a4(243) -> 244*
9.23/2.50	     a4(238) -> 239*
9.23/2.50	     a4(208) -> 209*
9.23/2.50	     a4(188) -> 189*
9.23/2.50	     a4(163) -> 164*
9.23/2.50	     a4(310) -> 311*
9.23/2.50	     a4(300) -> 301*
9.23/2.50	     a4(245) -> 246*
9.23/2.50	     a4(235) -> 236*
9.23/2.50	     a4(210) -> 211*
9.23/2.50	     a4(190) -> 191*
9.23/2.50	     a4(160) -> 161*
9.23/2.50	     a4(342) -> 343*
9.23/2.50	     a4(307) -> 308*
9.23/2.50	     a4(297) -> 298*
9.23/2.50	     a0(2) -> 1*
9.23/2.50	     a0(1) -> 1*
9.23/2.50	     b5(277) -> 278*
9.23/2.50	     b5(439) -> 440*
9.23/2.50	     b5(369) -> 370*
9.23/2.50	     b5(339) -> 340*
9.23/2.50	     b5(284) -> 285*
9.23/2.50	     b5(441) -> 442*
9.23/2.50	     b5(376) -> 377*
9.23/2.50	     b5(286) -> 287*
9.23/2.50	     b5(276) -> 277*
9.23/2.50	     b5(378) -> 379*
9.23/2.50	     b5(368) -> 369*
9.23/2.50	     b5(338) -> 339*
9.23/2.50	     b5(440) -> 441*
9.23/2.50	     b5(340) -> 341*
9.23/2.50	     b5(285) -> 286*
9.23/2.50	     b5(275) -> 276*
9.23/2.50	     b5(377) -> 378*
9.23/2.50	     b5(367) -> 368*
9.23/2.50	     b0(2) -> 2*
9.23/2.50	     b0(1) -> 2*
9.23/2.50	     a5(282) -> 283*
9.23/2.50	     a5(272) -> 273*
9.23/2.50	     a5(434) -> 435*
9.23/2.50	     a5(374) -> 375*
9.23/2.50	     a5(364) -> 365*
9.23/2.50	     a5(334) -> 335*
9.23/2.50	     a5(279) -> 280*
9.23/2.50	     a5(274) -> 275*
9.23/2.50	     a5(436) -> 437*
9.23/2.50	     a5(371) -> 372*
9.23/2.50	     a5(366) -> 367*
9.23/2.50	     a5(336) -> 337*
9.23/2.50	     a5(281) -> 282*
9.23/2.50	     a5(271) -> 272*
9.23/2.50	     a5(438) -> 439*
9.23/2.50	     a5(373) -> 374*
9.23/2.50	     a5(363) -> 364*
9.23/2.50	     a5(333) -> 334*
9.23/2.50	     a5(283) -> 284*
9.23/2.50	     a5(273) -> 274*
9.23/2.50	     a5(435) -> 436*
9.23/2.50	     a5(375) -> 376*
9.23/2.50	     a5(365) -> 366*
9.23/2.50	     a5(335) -> 336*
9.23/2.50	     a5(280) -> 281*
9.23/2.50	     a5(270) -> 271*
9.23/2.50	     a5(437) -> 438*
9.23/2.50	     a5(372) -> 373*
9.23/2.50	     a5(362) -> 363*
9.23/2.50	     a5(337) -> 338*
9.23/2.50	     b1(10) -> 11*
9.23/2.50	     b1(9) -> 10*
9.23/2.50	     b1(11) -> 12*
9.23/2.50	     b6(414) -> 415*
9.23/2.50	     b6(404) -> 405*
9.23/2.50	     b6(413) -> 414*
9.23/2.50	     b6(403) -> 404*
9.23/2.50	     b6(405) -> 406*
9.23/2.50	     b6(412) -> 413*
9.23/2.50	     a1(35) -> 36*
9.23/2.50	     a1(5) -> 6*
9.23/2.50	     a1(37) -> 38*
9.23/2.50	     a1(7) -> 8*
9.23/2.50	     a1(4) -> 5*
9.23/2.50	     a1(31) -> 32*
9.23/2.50	     a1(6) -> 7*
9.23/2.50	     a1(8) -> 9*
9.23/2.50	     a6(409) -> 410*
9.23/2.50	     a6(399) -> 400*
9.23/2.50	     a6(411) -> 412*
9.23/2.50	     a6(401) -> 402*
9.23/2.50	     a6(408) -> 409*
9.23/2.50	     a6(398) -> 399*
9.23/2.50	     a6(410) -> 411*
9.23/2.50	     a6(400) -> 401*
9.23/2.50	     a6(407) -> 408*
9.23/2.50	     a6(402) -> 403*
9.23/2.50	     b2(55) -> 56*
9.23/2.50	     b2(62) -> 63*
9.23/2.50	     b2(64) -> 65*
9.23/2.50	     b2(54) -> 55*
9.23/2.50	     b2(63) -> 64*
9.23/2.50	     b2(53) -> 54*
9.23/2.50	     a2(70) -> 71*
9.23/2.50	     a2(60) -> 61*
9.23/2.50	     a2(50) -> 51*
9.23/2.50	     a2(112) -> 113*
9.23/2.50	     a2(92) -> 93*
9.23/2.50	     a2(57) -> 58*
9.23/2.50	     a2(52) -> 53*
9.23/2.50	     a2(59) -> 60*
9.23/2.50	     a2(49) -> 50*
9.23/2.50	     a2(61) -> 62*
9.23/2.50	     a2(51) -> 52*
9.23/2.50	     a2(58) -> 59*
9.23/2.50	     a2(48) -> 49*
9.23/2.50	     b3(222) -> 223*
9.23/2.50	     b3(147) -> 148*
9.23/2.50	     b3(127) -> 128*
9.23/2.50	     b3(184) -> 185*
9.23/2.50	     b3(149) -> 150*
9.23/2.50	     b3(99) -> 100*
9.23/2.50	     b3(221) -> 222*
9.23/2.50	     b3(126) -> 127*
9.23/2.50	     b3(101) -> 102*
9.23/2.50	     b3(223) -> 224*
9.23/2.50	     b3(183) -> 184*
9.23/2.50	     b3(148) -> 149*
9.23/2.50	     b3(185) -> 186*
9.23/2.50	     b3(125) -> 126*
9.23/2.50	     b3(100) -> 101*
9.23/2.50	     1 -> 31*
9.23/2.50	     2 -> 4*
9.23/2.50	     9 -> 70*
9.23/2.50	     10 -> 48,37
9.23/2.50	     11 -> 35*
9.23/2.50	     12 -> 6,32,1
9.23/2.50	     32 -> 5*
9.23/2.50	     36 -> 5*
9.23/2.50	     38 -> 5*
9.23/2.50	     54 -> 129,57
9.23/2.50	     56 -> 50,7,8,6
9.23/2.50	     62 -> 116*
9.23/2.50	     63 -> 94,92
9.23/2.50	     64 -> 112*
9.23/2.50	     65 -> 71,9,8
9.23/2.50	     71 -> 49*
9.23/2.50	     93 -> 58*
9.23/2.50	     100 -> 120*
9.23/2.50	     102 -> 50,51
9.23/2.50	     113 -> 49*
9.23/2.50	     117 -> 95*
9.23/2.50	     125 -> 160*
9.23/2.50	     127 -> 142*
9.23/2.50	     128 -> 53,52
9.23/2.50	     130 -> 121*
9.23/2.50	     148 -> 187,178
9.23/2.50	     150 -> 122,59
9.23/2.50	     166 -> 207*
9.23/2.50	     168 -> 144*
9.23/2.50	     184 -> 216*
9.23/2.50	     186 -> 61*
9.23/2.50	     193 -> 234*
9.23/2.50	     195 -> 124*
9.23/2.50	     215 -> 146*
9.23/2.50	     222 -> 243*
9.23/2.50	     224 -> 117*
9.23/2.50	     240 -> 270*
9.23/2.50	     242 -> 161*
9.23/2.50	     249 -> 297*
9.23/2.50	     251 -> 97*
9.23/2.50	     276 -> 279*
9.23/2.50	     278 -> 163*
9.23/2.50	     284 -> 398*
9.23/2.50	     286 -> 333*
9.23/2.50	     287 -> 165*
9.23/2.50	     302 -> 362*
9.23/2.50	     304 -> 306*
9.23/2.50	     305 -> 99*
9.23/2.50	     312 -> 342*
9.23/2.50	     314 -> 122*
9.23/2.50	     339 -> 371*
9.23/2.50	     341 -> 209*
9.23/2.50	     343 -> 188*
9.23/2.50	     368 -> 434*
9.23/2.50	     370 -> 308*
9.23/2.50	     379 -> 211*
9.23/2.50	     404 -> 407*
9.23/2.50	     406 -> 335*
9.23/2.50	     415 -> 337*
9.23/2.50	     442 -> 310*
9.23/2.50	   problem:
9.23/2.50	    strict:
9.23/2.50	     
9.23/2.50	    weak:
9.23/2.50	     a(a(b(b(x1)))) -> b(b(b(a(a(a(a(a(x1))))))))
9.23/2.50	   Qed
9.23/2.51	EOF