YES(?,O(n^1))
0.16/0.43	YES(?,O(n^1))
0.16/0.43	
0.16/0.43	Problem:
0.16/0.43	 a(a(a(b(b(b(x1)))))) -> b(b(b(b(a(a(a(a(x1))))))))
0.16/0.43	
0.16/0.43	Proof:
0.16/0.43	 Bounds Processor:
0.16/0.43	  bound: 5
0.16/0.43	  enrichment: match
0.16/0.43	  automaton:
0.16/0.43	   final states: {3}
0.16/0.43	   transitions:
0.16/0.43	    a3(202) -> 203*
0.16/0.43	    a3(182) -> 183*
0.16/0.43	    a3(142) -> 143*
0.16/0.43	    a3(199) -> 200*
0.16/0.43	    a3(189) -> 190*
0.16/0.43	    a3(179) -> 180*
0.16/0.43	    a3(139) -> 140*
0.16/0.43	    a3(201) -> 202*
0.16/0.43	    a3(191) -> 192*
0.16/0.43	    a3(181) -> 182*
0.16/0.43	    a3(166) -> 167*
0.16/0.43	    a3(141) -> 142*
0.16/0.43	    a3(188) -> 189*
0.16/0.43	    a3(200) -> 201*
0.16/0.43	    a3(190) -> 191*
0.16/0.43	    a3(180) -> 181*
0.16/0.43	    a3(140) -> 141*
0.16/0.43	    b4(232) -> 233*
0.16/0.43	    b4(249) -> 250*
0.16/0.43	    b4(251) -> 252*
0.16/0.43	    b4(231) -> 232*
0.16/0.43	    b4(248) -> 249*
0.16/0.43	    b4(233) -> 234*
0.16/0.43	    b4(250) -> 251*
0.16/0.43	    b4(230) -> 231*
0.16/0.43	    a4(247) -> 248*
0.16/0.43	    a4(227) -> 228*
0.16/0.43	    a4(244) -> 245*
0.16/0.43	    a4(229) -> 230*
0.16/0.43	    a4(246) -> 247*
0.16/0.43	    a4(226) -> 227*
0.16/0.43	    a4(228) -> 229*
0.16/0.43	    a4(245) -> 246*
0.16/0.43	    a0(3) -> 3*
0.16/0.43	    b5(257) -> 258*
0.16/0.43	    b5(259) -> 260*
0.16/0.43	    b5(258) -> 259*
0.16/0.43	    b5(260) -> 261*
0.16/0.43	    b0(3) -> 3*
0.16/0.43	    a5(254) -> 255*
0.16/0.43	    a5(256) -> 257*
0.16/0.43	    a5(253) -> 254*
0.16/0.43	    a5(255) -> 256*
0.16/0.43	    b1(20) -> 21*
0.16/0.43	    b1(27) -> 28*
0.16/0.43	    b1(17) -> 18*
0.16/0.43	    b1(29) -> 30*
0.16/0.43	    b1(19) -> 20*
0.16/0.43	    b1(26) -> 27*
0.16/0.43	    b1(28) -> 29*
0.16/0.43	    b1(18) -> 19*
0.16/0.43	    a1(25) -> 26*
0.16/0.43	    a1(15) -> 16*
0.16/0.43	    a1(42) -> 43*
0.16/0.43	    a1(22) -> 23*
0.16/0.43	    a1(44) -> 45*
0.16/0.43	    a1(24) -> 25*
0.16/0.43	    a1(14) -> 15*
0.16/0.43	    a1(91) -> 92*
0.16/0.43	    a1(16) -> 17*
0.16/0.43	    a1(83) -> 84*
0.16/0.43	    a1(23) -> 24*
0.16/0.43	    a1(13) -> 14*
0.16/0.43	    a1(85) -> 86*
0.16/0.43	    b2(75) -> 76*
0.16/0.43	    b2(65) -> 66*
0.16/0.43	    b2(152) -> 153*
0.16/0.43	    b2(97) -> 98*
0.16/0.43	    b2(72) -> 73*
0.16/0.43	    b2(154) -> 155*
0.16/0.43	    b2(99) -> 100*
0.16/0.43	    b2(74) -> 75*
0.16/0.43	    b2(64) -> 65*
0.16/0.43	    b2(66) -> 67*
0.16/0.43	    b2(153) -> 154*
0.16/0.43	    b2(98) -> 99*
0.16/0.43	    b2(73) -> 74*
0.16/0.43	    b2(63) -> 64*
0.16/0.43	    b2(155) -> 156*
0.16/0.43	    b2(100) -> 101*
0.16/0.43	    a2(70) -> 71*
0.16/0.43	    a2(60) -> 61*
0.16/0.43	    a2(77) -> 78*
0.16/0.43	    a2(62) -> 63*
0.16/0.43	    a2(149) -> 150*
0.16/0.43	    a2(129) -> 130*
0.16/0.43	    a2(94) -> 95*
0.16/0.43	    a2(69) -> 70*
0.16/0.43	    a2(59) -> 60*
0.16/0.43	    a2(151) -> 152*
0.16/0.43	    a2(131) -> 132*
0.16/0.43	    a2(96) -> 97*
0.16/0.43	    a2(71) -> 72*
0.16/0.43	    a2(61) -> 62*
0.16/0.43	    a2(148) -> 149*
0.16/0.43	    a2(93) -> 94*
0.16/0.43	    a2(68) -> 69*
0.16/0.43	    a2(150) -> 151*
0.16/0.43	    a2(135) -> 136*
0.16/0.43	    a2(95) -> 96*
0.16/0.43	    b3(192) -> 193*
0.16/0.43	    b3(204) -> 205*
0.16/0.43	    b3(194) -> 195*
0.16/0.43	    b3(184) -> 185*
0.16/0.43	    b3(144) -> 145*
0.16/0.43	    b3(206) -> 207*
0.16/0.43	    b3(186) -> 187*
0.16/0.43	    b3(146) -> 147*
0.16/0.43	    b3(203) -> 204*
0.16/0.43	    b3(193) -> 194*
0.16/0.43	    b3(183) -> 184*
0.16/0.43	    b3(143) -> 144*
0.16/0.43	    b3(205) -> 206*
0.16/0.43	    b3(195) -> 196*
0.16/0.43	    b3(185) -> 186*
0.16/0.43	    b3(145) -> 146*
0.16/0.43	    3 -> 13*
0.16/0.43	    17 -> 68*
0.16/0.43	    18 -> 59,22
0.16/0.43	    19 -> 42*
0.16/0.43	    20 -> 44*
0.16/0.43	    21 -> 16,14,15,3
0.16/0.43	    26 -> 135*
0.16/0.43	    27 -> 83,77
0.16/0.43	    28 -> 85*
0.16/0.43	    29 -> 91*
0.16/0.43	    30 -> 16,14,3,15
0.16/0.43	    43 -> 23*
0.16/0.43	    45 -> 23*
0.16/0.43	    63 -> 166*
0.16/0.43	    64 -> 139,93
0.16/0.43	    65 -> 131*
0.16/0.43	    66 -> 129*
0.16/0.43	    67 -> 69,70,17,16
0.16/0.43	    73 -> 199,148
0.16/0.43	    76 -> 62,25
0.16/0.43	    78 -> 60*
0.16/0.43	    84 -> 14*
0.16/0.43	    86 -> 14*
0.16/0.43	    92 -> 14*
0.16/0.43	    101 -> 70*
0.16/0.43	    130 -> 69*
0.16/0.43	    132 -> 69*
0.16/0.43	    136 -> 60*
0.16/0.43	    145 -> 188*
0.16/0.43	    147 -> 72,71
0.16/0.43	    153 -> 179*
0.16/0.43	    156 -> 61*
0.16/0.43	    167 -> 140*
0.16/0.43	    184 -> 226*
0.16/0.43	    187 -> 167,140
0.16/0.43	    196 -> 202,151
0.16/0.43	    207 -> 141*
0.16/0.43	    230 -> 253*
0.16/0.43	    233 -> 244*
0.16/0.43	    234 -> 143*
0.16/0.43	    252 -> 191*
0.16/0.43	    261 -> 247*
0.16/0.43	  problem:
0.16/0.43	   
0.16/0.43	  Qed
0.16/0.43	EOF