YES(?,O(n^1))
3.10/1.09	YES(?,O(n^1))
3.10/1.10	
3.10/1.10	Problem:
3.10/1.10	 a(c(b(x1))) -> b(a(b(a(x1))))
3.10/1.10	 b(x1) -> c(a(c(x1)))
3.10/1.10	 a(a(x1)) -> a(b(c(a(x1))))
3.10/1.10	
3.10/1.10	Proof:
3.10/1.10	 Bounds Processor:
3.10/1.10	  bound: 5
3.10/1.10	  enrichment: match
3.10/1.10	  automaton:
3.10/1.10	   final states: {4}
3.10/1.10	   transitions:
3.10/1.10	    a3(262) -> 263*
3.10/1.10	    a3(192) -> 193*
3.10/1.10	    a3(122) -> 123*
3.10/1.10	    a3(189) -> 190*
3.10/1.10	    a3(179) -> 180*
3.10/1.10	    a3(159) -> 160*
3.10/1.10	    a3(236) -> 237*
3.10/1.10	    a3(166) -> 167*
3.10/1.10	    a3(243) -> 244*
3.10/1.10	    a3(148) -> 149*
3.10/1.10	    a3(210) -> 211*
3.10/1.10	    a3(170) -> 171*
3.10/1.10	    a3(150) -> 151*
3.10/1.10	    a3(130) -> 131*
3.10/1.10	    a3(105) -> 106*
3.10/1.10	    b3(149) -> 150*
3.10/1.10	    b3(261) -> 262*
3.10/1.10	    b3(191) -> 192*
3.10/1.10	    b3(151) -> 152*
3.10/1.10	    c4(227) -> 228*
3.10/1.10	    c4(212) -> 213*
3.10/1.10	    c4(264) -> 265*
3.10/1.10	    c4(239) -> 240*
3.10/1.10	    c4(214) -> 215*
3.10/1.10	    c4(266) -> 267*
3.10/1.10	    c4(241) -> 242*
3.10/1.10	    c4(250) -> 251*
3.10/1.10	    c4(225) -> 226*
3.10/1.10	    a4(252) -> 253*
3.10/1.10	    a4(249) -> 250*
3.10/1.10	    a4(226) -> 227*
3.10/1.10	    a4(213) -> 214*
3.10/1.10	    a4(265) -> 266*
3.10/1.10	    a4(240) -> 241*
3.10/1.10	    a0(4) -> 4*
3.10/1.10	    b4(251) -> 252*
3.10/1.10	    c0(4) -> 4*
3.10/1.10	    c5(276) -> 277*
3.10/1.10	    c5(278) -> 279*
3.10/1.10	    b0(4) -> 4*
3.10/1.10	    a5(277) -> 278*
3.10/1.10	    a1(247) -> 248*
3.10/1.10	    a1(25) -> 26*
3.10/1.10	    a1(10) -> 11*
3.10/1.10	    a1(27) -> 28*
3.10/1.10	    a1(12) -> 13*
3.10/1.10	    a1(29) -> 30*
3.10/1.10	    a1(16) -> 17*
3.10/1.10	    a1(98) -> 99*
3.10/1.10	    a1(100) -> 101*
3.10/1.10	    b1(30) -> 31*
3.10/1.10	    b1(24) -> 25*
3.10/1.10	    b1(11) -> 12*
3.10/1.10	    b1(28) -> 29*
3.10/1.10	    b1(13) -> 14*
3.10/1.10	    c1(15) -> 16*
3.10/1.10	    c1(17) -> 18*
3.10/1.10	    c1(23) -> 24*
3.10/1.10	    a2(75) -> 76*
3.10/1.10	    a2(55) -> 56*
3.10/1.10	    a2(182) -> 183*
3.10/1.10	    a2(102) -> 103*
3.10/1.10	    a2(109) -> 110*
3.10/1.10	    a2(59) -> 60*
3.10/1.10	    a2(44) -> 45*
3.10/1.10	    a2(196) -> 197*
3.10/1.10	    a2(46) -> 47*
3.10/1.10	    a2(138) -> 139*
3.10/1.10	    a2(118) -> 119*
3.10/1.10	    a2(88) -> 89*
3.10/1.10	    a2(280) -> 281*
3.10/1.10	    a2(78) -> 79*
3.10/1.10	    a2(68) -> 69*
3.10/1.10	    a2(200) -> 201*
3.10/1.10	    a2(135) -> 136*
3.10/1.10	    a2(90) -> 91*
3.10/1.10	    b2(45) -> 46*
3.10/1.10	    b2(137) -> 138*
3.10/1.10	    b2(77) -> 78*
3.10/1.10	    b2(47) -> 48*
3.10/1.10	    b2(89) -> 90*
3.10/1.10	    b2(91) -> 92*
3.10/1.10	    b2(195) -> 196*
3.10/1.10	    c2(60) -> 61*
3.10/1.10	    c2(117) -> 118*
3.10/1.10	    c2(67) -> 68*
3.10/1.10	    c2(194) -> 195*
3.10/1.10	    c2(119) -> 120*
3.10/1.10	    c2(69) -> 70*
3.10/1.10	    c2(54) -> 55*
3.10/1.10	    c2(136) -> 137*
3.10/1.10	    c2(76) -> 77*
3.10/1.10	    c2(56) -> 57*
3.10/1.10	    c2(108) -> 109*
3.10/1.10	    c2(58) -> 59*
3.10/1.10	    c2(110) -> 111*
3.10/1.10	    c3(237) -> 238*
3.10/1.10	    c3(167) -> 168*
3.10/1.10	    c3(169) -> 170*
3.10/1.10	    c3(129) -> 130*
3.10/1.10	    c3(104) -> 105*
3.10/1.10	    c3(171) -> 172*
3.10/1.10	    c3(131) -> 132*
3.10/1.10	    c3(121) -> 122*
3.10/1.10	    c3(106) -> 107*
3.10/1.10	    c3(178) -> 179*
3.10/1.10	    c3(123) -> 124*
3.10/1.10	    c3(260) -> 261*
3.10/1.10	    c3(235) -> 236*
3.10/1.10	    c3(190) -> 191*
3.10/1.10	    c3(180) -> 181*
3.10/1.10	    c3(165) -> 166*
3.10/1.10	    4 -> 15,10
3.10/1.10	    11 -> 54,23
3.10/1.10	    12 -> 135*
3.10/1.10	    13 -> 58,44,27
3.10/1.10	    14 -> 11,17,23,4
3.10/1.10	    18 -> 4*
3.10/1.10	    24 -> 67*
3.10/1.10	    25 -> 75*
3.10/1.10	    26 -> 11,23,4
3.10/1.10	    28 -> 117*
3.10/1.10	    29 -> 182*
3.10/1.10	    30 -> 108,102,98
3.10/1.10	    31 -> 11,4,23
3.10/1.10	    45 -> 129*
3.10/1.10	    46 -> 189*
3.10/1.10	    47 -> 194,148,121,100,88
3.10/1.10	    48 -> 56,11,17
3.10/1.10	    57 -> 12*
3.10/1.10	    61 -> 14,4
3.10/1.10	    70 -> 25*
3.10/1.10	    77 -> 104*
3.10/1.10	    79 -> 248,11,23
3.10/1.10	    89 -> 169*
3.10/1.10	    90 -> 243*
3.10/1.10	    91 -> 165,159
3.10/1.10	    92 -> 13,11
3.10/1.10	    99 -> 11*
3.10/1.10	    101 -> 11*
3.10/1.10	    103 -> 45*
3.10/1.10	    107 -> 78*
3.10/1.10	    111 -> 31*
3.10/1.10	    120 -> 29*
3.10/1.10	    124 -> 48,17
3.10/1.10	    132 -> 46*
3.10/1.10	    137 -> 178*
3.10/1.10	    139 -> 103,99,11,23,45,28
3.10/1.10	    149 -> 239*
3.10/1.10	    150 -> 280,249
3.10/1.10	    151 -> 260,247,225,210,200
3.10/1.10	    152 -> 60,56,136
3.10/1.10	    160 -> 149*
3.10/1.10	    168 -> 92*
3.10/1.10	    172 -> 90*
3.10/1.10	    181 -> 138*
3.10/1.10	    183 -> 136*
3.10/1.10	    191 -> 212*
3.10/1.10	    193 -> 160,149,89
3.10/1.10	    195 -> 235*
3.10/1.10	    197 -> 101*
3.10/1.10	    201 -> 89*
3.10/1.10	    211 -> 149*
3.10/1.10	    215 -> 192*
3.10/1.10	    228 -> 152,56,136
3.10/1.10	    238 -> 196*
3.10/1.10	    242 -> 150*
3.10/1.10	    244 -> 190*
3.10/1.10	    248 -> 11*
3.10/1.10	    251 -> 276*
3.10/1.10	    253 -> 211*
3.10/1.10	    261 -> 264*
3.10/1.10	    263 -> 201*
3.10/1.10	    267 -> 262*
3.10/1.10	    279 -> 252*
3.10/1.10	    281 -> 76*
3.10/1.10	  problem:
3.10/1.10	   
3.10/1.10	  Qed
3.10/1.10	EOF