YES(?,O(n^1))
0.16/0.98	YES(?,O(n^1))
0.16/0.99	
0.16/0.99	Problem:
0.16/0.99	 a(a(b(b(x1)))) -> b(b(b(a(a(a(x1))))))
0.16/0.99	
0.16/0.99	Proof:
0.16/0.99	 Bounds Processor:
0.16/0.99	  bound: 5
0.16/0.99	  enrichment: match
0.16/0.99	  automaton:
0.16/0.99	   final states: {3}
0.16/0.99	   transitions:
0.16/0.99	    a3(172) -> 173*
0.16/0.99	    a3(157) -> 158*
0.16/0.99	    a3(142) -> 143*
0.16/0.99	    a3(92) -> 93*
0.16/0.99	    a3(199) -> 200*
0.16/0.99	    a3(149) -> 150*
0.16/0.99	    a3(139) -> 140*
0.16/0.99	    a3(94) -> 95*
0.16/0.99	    a3(201) -> 202*
0.16/0.99	    a3(171) -> 172*
0.16/0.99	    a3(156) -> 157*
0.16/0.99	    a3(141) -> 142*
0.16/0.99	    a3(173) -> 174*
0.16/0.99	    a3(148) -> 149*
0.16/0.99	    a3(143) -> 144*
0.16/0.99	    a3(93) -> 94*
0.16/0.99	    a3(200) -> 201*
0.16/0.99	    a3(155) -> 156*
0.16/0.99	    a3(150) -> 151*
0.16/0.99	    b4(232) -> 233*
0.16/0.99	    b4(197) -> 198*
0.16/0.99	    b4(182) -> 183*
0.16/0.99	    b4(239) -> 240*
0.16/0.99	    b4(234) -> 235*
0.16/0.99	    b4(219) -> 220*
0.16/0.99	    b4(241) -> 242*
0.16/0.99	    b4(196) -> 197*
0.16/0.99	    b4(181) -> 182*
0.16/0.99	    b4(233) -> 234*
0.16/0.99	    b4(218) -> 219*
0.16/0.99	    b4(183) -> 184*
0.16/0.99	    b4(240) -> 241*
0.16/0.99	    b4(220) -> 221*
0.16/0.99	    b4(195) -> 196*
0.16/0.99	    a4(237) -> 238*
0.16/0.99	    a4(217) -> 218*
0.16/0.99	    a4(192) -> 193*
0.16/0.99	    a4(229) -> 230*
0.16/0.99	    a4(194) -> 195*
0.16/0.99	    a4(179) -> 180*
0.16/0.99	    a4(236) -> 237*
0.16/0.99	    a4(231) -> 232*
0.16/0.99	    a4(216) -> 217*
0.16/0.99	    a4(238) -> 239*
0.16/0.99	    a4(193) -> 194*
0.16/0.99	    a4(178) -> 179*
0.16/0.99	    a4(230) -> 231*
0.16/0.99	    a4(215) -> 216*
0.16/0.99	    a4(180) -> 181*
0.16/0.99	    a0(3) -> 3*
0.16/0.99	    b5(254) -> 255*
0.16/0.99	    b5(253) -> 254*
0.16/0.99	    b5(255) -> 256*
0.16/0.99	    b0(3) -> 3*
0.16/0.99	    a5(252) -> 253*
0.16/0.99	    a5(251) -> 252*
0.16/0.99	    a5(250) -> 251*
0.16/0.99	    b1(15) -> 16*
0.16/0.99	    b1(22) -> 23*
0.16/0.99	    b1(14) -> 15*
0.16/0.99	    b1(21) -> 22*
0.16/0.99	    b1(16) -> 17*
0.16/0.99	    b1(23) -> 24*
0.16/0.99	    a1(65) -> 66*
0.16/0.99	    a1(20) -> 21*
0.16/0.99	    a1(67) -> 68*
0.16/0.99	    a1(12) -> 13*
0.16/0.99	    a1(34) -> 35*
0.16/0.99	    a1(19) -> 20*
0.16/0.99	    a1(11) -> 12*
0.16/0.99	    a1(18) -> 19*
0.16/0.99	    a1(13) -> 14*
0.16/0.99	    b2(55) -> 56*
0.16/0.99	    b2(50) -> 51*
0.16/0.99	    b2(122) -> 123*
0.16/0.99	    b2(112) -> 113*
0.16/0.99	    b2(57) -> 58*
0.16/0.99	    b2(124) -> 125*
0.16/0.99	    b2(79) -> 80*
0.16/0.99	    b2(49) -> 50*
0.16/0.99	    b2(111) -> 112*
0.16/0.99	    b2(81) -> 82*
0.16/0.99	    b2(56) -> 57*
0.16/0.99	    b2(123) -> 124*
0.16/0.99	    b2(113) -> 114*
0.16/0.99	    b2(48) -> 49*
0.16/0.99	    b2(80) -> 81*
0.16/0.99	    a2(45) -> 46*
0.16/0.99	    a2(77) -> 78*
0.16/0.99	    a2(52) -> 53*
0.16/0.99	    a2(47) -> 48*
0.16/0.99	    a2(119) -> 120*
0.16/0.99	    a2(109) -> 110*
0.16/0.99	    a2(59) -> 60*
0.16/0.99	    a2(54) -> 55*
0.16/0.99	    a2(126) -> 127*
0.16/0.99	    a2(121) -> 122*
0.16/0.99	    a2(76) -> 77*
0.16/0.99	    a2(46) -> 47*
0.16/0.99	    a2(108) -> 109*
0.16/0.99	    a2(83) -> 84*
0.16/0.99	    a2(78) -> 79*
0.16/0.99	    a2(53) -> 54*
0.16/0.99	    a2(120) -> 121*
0.16/0.99	    a2(110) -> 111*
0.16/0.99	    b3(202) -> 203*
0.16/0.99	    b3(152) -> 153*
0.16/0.99	    b3(97) -> 98*
0.16/0.99	    b3(204) -> 205*
0.16/0.99	    b3(174) -> 175*
0.16/0.99	    b3(159) -> 160*
0.16/0.99	    b3(144) -> 145*
0.16/0.99	    b3(176) -> 177*
0.16/0.99	    b3(151) -> 152*
0.16/0.99	    b3(146) -> 147*
0.16/0.99	    b3(96) -> 97*
0.16/0.99	    b3(203) -> 204*
0.16/0.99	    b3(158) -> 159*
0.16/0.99	    b3(153) -> 154*
0.16/0.99	    b3(175) -> 176*
0.16/0.99	    b3(160) -> 161*
0.16/0.99	    b3(145) -> 146*
0.16/0.99	    b3(95) -> 96*
0.16/0.99	    3 -> 11*
0.16/0.99	    14 -> 52*
0.16/0.99	    15 -> 45,18
0.16/0.99	    16 -> 34*
0.16/0.99	    17 -> 13,12,3
0.16/0.99	    21 -> 83*
0.16/0.99	    22 -> 65,59
0.16/0.99	    23 -> 67*
0.16/0.99	    24 -> 13,3,11,12
0.16/0.99	    35 -> 19*
0.16/0.99	    48 -> 141*
0.16/0.99	    49 -> 108,92
0.16/0.99	    50 -> 76*
0.16/0.99	    51 -> 53,14,13
0.16/0.99	    56 -> 119*
0.16/0.99	    58 -> 20*
0.16/0.99	    60 -> 46*
0.16/0.99	    66 -> 12*
0.16/0.99	    68 -> 12*
0.16/0.99	    80 -> 171,126
0.16/0.99	    82 -> 20,47
0.16/0.99	    84 -> 46*
0.16/0.99	    95 -> 178*
0.16/0.99	    97 -> 155*
0.16/0.99	    98 -> 55,54
0.16/0.99	    112 -> 139*
0.16/0.99	    114 -> 53*
0.16/0.99	    123 -> 148*
0.16/0.99	    125 -> 84,46
0.16/0.99	    127 -> 120*
0.16/0.99	    140 -> 93*
0.16/0.99	    147 -> 78*
0.16/0.99	    151 -> 229*
0.16/0.99	    152 -> 215*
0.16/0.99	    153 -> 199*
0.16/0.99	    154 -> 48*
0.16/0.99	    161 -> 121*
0.16/0.99	    175 -> 192*
0.16/0.99	    177 -> 142*
0.16/0.99	    184 -> 157*
0.16/0.99	    198 -> 144*
0.16/0.99	    203 -> 236*
0.16/0.99	    205 -> 94,110
0.16/0.99	    221 -> 143*
0.16/0.99	    235 -> 201*
0.16/0.99	    240 -> 250*
0.16/0.99	    242 -> 179*
0.16/0.99	    256 -> 181*
0.16/0.99	  problem:
0.16/0.99	   
0.16/0.99	  Qed
0.16/0.99	EOF