YES(?,O(n^1))
0.16/0.46	YES(?,O(n^1))
0.16/0.46	
0.16/0.46	Problem:
0.16/0.46	 b(c(a(x1))) -> a(b(a(b(c(x1)))))
0.16/0.46	 b(x1) -> c(c(x1))
0.16/0.46	 c(d(x1)) -> a(b(c(a(x1))))
0.16/0.46	 a(a(x1)) -> a(c(b(a(x1))))
0.16/0.46	
0.16/0.46	Proof:
0.16/0.46	 Bounds Processor:
0.16/0.46	  bound: 4
0.16/0.46	  enrichment: match
0.16/0.46	  automaton:
0.16/0.46	   final states: {6,5}
0.16/0.46	   transitions:
0.16/0.46	    b3(137) -> 138*
0.16/0.46	    b3(184) -> 185*
0.16/0.46	    b3(179) -> 180*
0.16/0.46	    b3(139) -> 140*
0.16/0.46	    b3(311) -> 312*
0.16/0.46	    b3(226) -> 227*
0.16/0.46	    b3(186) -> 187*
0.16/0.46	    b3(240) -> 241*
0.16/0.46	    a1(15) -> 16*
0.16/0.46	    a1(17) -> 18*
0.16/0.46	    a1(261) -> 262*
0.16/0.46	    a1(36) -> 37*
0.16/0.46	    a1(320) -> 321*
0.16/0.46	    a1(33) -> 34*
0.16/0.46	    c4(217) -> 218*
0.16/0.46	    c4(299) -> 300*
0.16/0.46	    c4(219) -> 220*
0.16/0.46	    c4(326) -> 327*
0.16/0.46	    c4(291) -> 292*
0.16/0.46	    c4(216) -> 217*
0.16/0.46	    c4(206) -> 207*
0.16/0.46	    c4(303) -> 304*
0.16/0.46	    c4(288) -> 289*
0.16/0.46	    c4(300) -> 301*
0.16/0.46	    c4(290) -> 291*
0.16/0.46	    c4(220) -> 221*
0.16/0.46	    c4(205) -> 206*
0.16/0.46	    c4(302) -> 303*
0.16/0.46	    c4(287) -> 288*
0.16/0.46	    c1(277) -> 278*
0.16/0.46	    c1(60) -> 61*
0.16/0.46	    c1(25) -> 26*
0.16/0.46	    c1(27) -> 28*
0.16/0.46	    c1(34) -> 35*
0.16/0.46	    c1(19) -> 20*
0.16/0.46	    c1(191) -> 192*
0.16/0.46	    c1(43) -> 44*
0.16/0.46	    c1(13) -> 14*
0.16/0.46	    b1(42) -> 43*
0.16/0.46	    b1(14) -> 15*
0.16/0.46	    b1(16) -> 17*
0.16/0.46	    a2(70) -> 71*
0.16/0.46	    a2(47) -> 48*
0.16/0.46	    a2(174) -> 175*
0.16/0.46	    a2(104) -> 105*
0.16/0.46	    a2(49) -> 50*
0.16/0.46	    a2(166) -> 167*
0.16/0.46	    a2(101) -> 102*
0.16/0.46	    a2(68) -> 69*
0.16/0.46	    c2(45) -> 46*
0.16/0.46	    c2(92) -> 93*
0.16/0.46	    c2(82) -> 83*
0.16/0.46	    c2(244) -> 245*
0.16/0.46	    c2(189) -> 190*
0.16/0.46	    c2(79) -> 80*
0.16/0.46	    c2(201) -> 202*
0.16/0.46	    c2(131) -> 132*
0.16/0.46	    c2(81) -> 82*
0.16/0.46	    c2(66) -> 67*
0.16/0.46	    c2(173) -> 174*
0.16/0.46	    c2(123) -> 124*
0.16/0.46	    c2(103) -> 104*
0.16/0.46	    c2(93) -> 94*
0.16/0.46	    c2(78) -> 79*
0.16/0.46	    c2(275) -> 276*
0.16/0.46	    c2(58) -> 59*
0.16/0.46	    c2(165) -> 166*
0.16/0.46	    b0(5) -> 5*
0.16/0.46	    b0(6) -> 5*
0.16/0.46	    b2(172) -> 173*
0.16/0.46	    b2(102) -> 103*
0.16/0.46	    b2(67) -> 68*
0.16/0.46	    b2(164) -> 165*
0.16/0.46	    b2(69) -> 70*
0.16/0.46	    b2(46) -> 47*
0.16/0.46	    b2(48) -> 49*
0.16/0.46	    c0(5) -> 5*
0.16/0.46	    c0(6) -> 5*
0.16/0.46	    a3(242) -> 243*
0.16/0.46	    a3(187) -> 188*
0.16/0.46	    a3(181) -> 182*
0.16/0.46	    a3(313) -> 314*
0.16/0.46	    a3(228) -> 229*
0.16/0.46	    a3(178) -> 179*
0.16/0.46	    a3(138) -> 139*
0.16/0.46	    a3(230) -> 231*
0.16/0.46	    a3(225) -> 226*
0.16/0.46	    a3(185) -> 186*
0.16/0.46	    a3(140) -> 141*
0.16/0.46	    a0(5) -> 5*
0.16/0.46	    a0(6) -> 5*
0.16/0.46	    c3(227) -> 228*
0.16/0.46	    c3(157) -> 158*
0.16/0.46	    c3(142) -> 143*
0.16/0.46	    c3(269) -> 270*
0.16/0.46	    c3(214) -> 215*
0.16/0.46	    c3(159) -> 160*
0.16/0.46	    c3(149) -> 150*
0.16/0.46	    c3(241) -> 242*
0.16/0.46	    c3(211) -> 212*
0.16/0.46	    c3(156) -> 157*
0.16/0.46	    c3(146) -> 147*
0.16/0.46	    c3(136) -> 137*
0.16/0.46	    c3(213) -> 214*
0.16/0.46	    c3(203) -> 204*
0.16/0.46	    c3(183) -> 184*
0.16/0.46	    c3(148) -> 149*
0.16/0.46	    c3(143) -> 144*
0.16/0.46	    c3(210) -> 211*
0.16/0.46	    c3(180) -> 181*
0.16/0.46	    c3(160) -> 161*
0.16/0.46	    c3(145) -> 146*
0.16/0.46	    d0(5) -> 6*
0.16/0.46	    d0(6) -> 6*
0.16/0.46	    5 -> 33,13
0.16/0.46	    6 -> 36,19
0.16/0.46	    14 -> 78,27
0.16/0.46	    16 -> 81*
0.16/0.46	    17 -> 101,66,60
0.16/0.46	    18 -> 46,47,34,42,20,25,14,27,15,5
0.16/0.46	    20 -> 25,14
0.16/0.46	    26 -> 5*
0.16/0.46	    28 -> 5*
0.16/0.46	    33 -> 58*
0.16/0.46	    34 -> 42*
0.16/0.46	    35 -> 16*
0.16/0.46	    36 -> 45*
0.16/0.46	    37 -> 34*
0.16/0.46	    42 -> 92*
0.16/0.46	    44 -> 17*
0.16/0.46	    46 -> 145*
0.16/0.46	    47 -> 244*
0.16/0.46	    48 -> 148*
0.16/0.46	    49 -> 178,136,131
0.16/0.46	    50 -> 15,172,17
0.16/0.46	    59 -> 46*
0.16/0.46	    61 -> 14*
0.16/0.46	    67 -> 142*
0.16/0.46	    69 -> 156*
0.16/0.46	    70 -> 225,203,201
0.16/0.46	    71 -> 164,17,47,15
0.16/0.46	    80 -> 15*
0.16/0.46	    83 -> 17*
0.16/0.46	    94 -> 43*
0.16/0.46	    102 -> 159*
0.16/0.46	    104 -> 123*
0.16/0.46	    105 -> 48,148,16,34,42
0.16/0.46	    124 -> 46*
0.16/0.46	    132 -> 67*
0.16/0.46	    137 -> 219*
0.16/0.46	    139 -> 216*
0.16/0.46	    141 -> 240,68
0.16/0.46	    144 -> 68*
0.16/0.46	    147 -> 47*
0.16/0.46	    150 -> 49*
0.16/0.46	    158 -> 70*
0.16/0.46	    161 -> 103*
0.16/0.46	    164 -> 213*
0.16/0.46	    166 -> 320,313,277,275,269
0.16/0.46	    167 -> 18,47,34,42,5,92,15,20,46,78,16
0.16/0.46	    172 -> 210*
0.16/0.46	    174 -> 261,230,191,189,183
0.16/0.46	    175 -> 16,81,18
0.16/0.46	    179 -> 205*
0.16/0.46	    182 -> 102*
0.16/0.46	    184 -> 302*
0.16/0.46	    186 -> 299*
0.16/0.46	    188 -> 311,47
0.16/0.46	    190 -> 46*
0.16/0.46	    192 -> 14*
0.16/0.46	    202 -> 67*
0.16/0.46	    204 -> 137*
0.16/0.46	    207 -> 180*
0.16/0.46	    212 -> 173*
0.16/0.46	    215 -> 165*
0.16/0.46	    218 -> 140*
0.16/0.46	    221 -> 138*
0.16/0.46	    226 -> 287*
0.16/0.46	    229 -> 48,102,159,148
0.16/0.46	    231 -> 226*
0.16/0.46	    240 -> 290*
0.16/0.46	    243 -> 69,156
0.16/0.46	    245 -> 104*
0.16/0.46	    262 -> 42*
0.16/0.46	    270 -> 184*
0.16/0.46	    276 -> 46*
0.16/0.46	    278 -> 14*
0.16/0.46	    289 -> 312,227
0.16/0.46	    292 -> 241*
0.16/0.46	    301 -> 187*
0.16/0.46	    304 -> 185*
0.16/0.46	    311 -> 326*
0.16/0.46	    312 -> 227*
0.16/0.46	    314 -> 226*
0.16/0.46	    321 -> 42*
0.16/0.46	    327 -> 288*
0.16/0.46	  problem:
0.16/0.46	   
0.16/0.46	  Qed
0.16/0.47	EOF