YES(?,O(n^1))
30.09/8.70	YES(?,O(n^1))
33.77/8.71	
33.77/8.71	Problem:
33.77/8.71	 active(g(X)) -> mark(h(X))
33.77/8.71	 active(c()) -> mark(d())
33.77/8.71	 active(h(d())) -> mark(g(c()))
33.77/8.71	 mark(g(X)) -> active(g(X))
33.77/8.71	 mark(h(X)) -> active(h(X))
33.77/8.71	 mark(c()) -> active(c())
33.77/8.71	 mark(d()) -> active(d())
33.77/8.71	 g(mark(X)) -> g(X)
33.77/8.71	 g(active(X)) -> g(X)
33.77/8.71	 h(mark(X)) -> h(X)
33.77/8.71	 h(active(X)) -> h(X)
33.77/8.71	
33.77/8.71	Proof:
33.77/8.71	 Bounds Processor:
33.77/8.71	  bound: 7
33.77/8.71	  enrichment: match
33.77/8.71	  automaton:
33.77/8.71	   final states: {7}
33.77/8.71	   transitions:
33.77/8.71	    active3(162) -> 163*
33.77/8.71	    active3(298) -> 299*
33.77/8.71	    active3(300) -> 301*
33.77/8.71	    active3(302) -> 303*
33.77/8.71	    d3() -> 200*
33.77/8.71	    g3(296) -> 297*
33.77/8.71	    g3(161) -> 162*
33.77/8.71	    mark3(125) -> 126*
33.77/8.71	    c3() -> 296*
33.77/8.71	    h4(511) -> 512*
33.77/8.71	    h4(668) -> 669*
33.77/8.71	    h4(259) -> 260*
33.77/8.71	    h4(426) -> 427*
33.77/8.71	    h4(583) -> 584*
33.77/8.71	    h4(513) -> 514*
33.77/8.71	    h4(670) -> 671*
33.77/8.71	    h4(418) -> 419*
33.77/8.71	    h4(338) -> 339*
33.77/8.71	    h4(515) -> 516*
33.77/8.71	    h4(647) -> 648*
33.77/8.71	    h4(719) -> 720*
33.77/8.71	    h4(507) -> 508*
33.77/8.71	    h4(509) -> 510*
33.77/8.71	    active4(339) -> 340*
33.77/8.71	    active0(7) -> 7*
33.77/8.71	    g4(458) -> 459*
33.77/8.71	    g4(460) -> 461*
33.77/8.71	    g0(7) -> 7*
33.77/8.71	    mark4(260) -> 261*
33.77/8.71	    mark0(7) -> 7*
33.77/8.71	    active5(477) -> 478*
33.77/8.71	    h0(7) -> 7*
33.77/8.71	    h5(476) -> 477*
33.77/8.71	    h5(517) -> 518*
33.77/8.71	    c0() -> 7*
33.77/8.71	    c4() -> 458*
33.77/8.71	    d0() -> 7*
33.77/8.71	    mark5(518) -> 519*
33.77/8.71	    h1(681) -> 682*
33.77/8.71	    h1(147) -> 148*
33.77/8.71	    h1(526) -> 527*
33.77/8.71	    h1(608) -> 609*
33.77/8.71	    h1(139) -> 140*
33.77/8.71	    h1(528) -> 529*
33.77/8.71	    h1(141) -> 142*
33.77/8.71	    h1(131) -> 132*
33.77/8.71	    h1(520) -> 521*
33.77/8.71	    h1(687) -> 688*
33.77/8.71	    h1(11) -> 12*
33.77/8.71	    h1(133) -> 134*
33.77/8.71	    h1(522) -> 523*
33.77/8.71	    h1(649) -> 650*
33.77/8.71	    h1(43) -> 44*
33.77/8.71	    h1(145) -> 146*
33.77/8.71	    h1(524) -> 525*
33.77/8.71	    h1(721) -> 722*
33.77/8.71	    g5(540) -> 541*
33.77/8.71	    g1(84) -> 85*
33.77/8.71	    g1(19) -> 20*
33.77/8.71	    g1(86) -> 87*
33.77/8.71	    g1(21) -> 22*
33.77/8.71	    active6(615) -> 616*
33.77/8.71	    active1(30) -> 31*
33.77/8.71	    active1(22) -> 23*
33.77/8.71	    active1(169) -> 170*
33.77/8.71	    active1(28) -> 29*
33.77/8.71	    active1(175) -> 176*
33.77/8.71	    h6(605) -> 606*
33.77/8.71	    h6(614) -> 615*
33.77/8.71	    d1() -> 14*
33.77/8.71	    mark6(606) -> 607*
33.77/8.71	    c1() -> 19*
33.77/8.71	    active7(654) -> 655*
33.77/8.71	    mark1(12) -> 13*
33.77/8.71	    h7(653) -> 654*
33.77/8.71	    h2(272) -> 273*
33.77/8.71	    h2(454) -> 455*
33.77/8.71	    h2(651) -> 652*
33.77/8.71	    h2(40) -> 41*
33.77/8.71	    h2(434) -> 435*
33.77/8.71	    h2(631) -> 632*
33.77/8.71	    h2(536) -> 537*
33.77/8.71	    h2(324) -> 325*
33.77/8.71	    h2(723) -> 724*
33.77/8.71	    h2(703) -> 704*
33.77/8.71	    h2(284) -> 285*
33.77/8.71	    h2(274) -> 275*
33.77/8.71	    h2(67) -> 68*
33.77/8.71	    h2(456) -> 457*
33.77/8.71	    h2(446) -> 447*
33.77/8.71	    h2(633) -> 634*
33.77/8.71	    h2(189) -> 190*
33.77/8.71	    h2(149) -> 150*
33.77/8.71	    h2(538) -> 539*
33.77/8.71	    h2(735) -> 736*
33.77/8.71	    h2(316) -> 317*
33.77/8.71	    h2(114) -> 115*
33.77/8.71	    h2(695) -> 696*
33.77/8.71	    h2(286) -> 287*
33.77/8.71	    h2(266) -> 267*
33.77/8.71	    h2(49) -> 50*
33.77/8.71	    h2(448) -> 449*
33.77/8.71	    h2(635) -> 636*
33.77/8.71	    h2(151) -> 152*
33.77/8.71	    h2(530) -> 531*
33.77/8.71	    h2(318) -> 319*
33.77/8.71	    h2(662) -> 663*
33.77/8.71	    h2(450) -> 451*
33.77/8.71	    h2(440) -> 441*
33.77/8.71	    h2(627) -> 628*
33.77/8.71	    h2(612) -> 613*
33.77/8.71	    h2(153) -> 154*
33.77/8.71	    h2(532) -> 533*
33.77/8.71	    h2(330) -> 331*
33.77/8.71	    h2(729) -> 730*
33.77/8.71	    h2(108) -> 109*
33.77/8.71	    h2(689) -> 690*
33.77/8.71	    h2(452) -> 453*
33.77/8.71	    h2(629) -> 630*
33.77/8.71	    h2(155) -> 156*
33.77/8.71	    h2(534) -> 535*
33.77/8.71	    h2(332) -> 333*
33.77/8.71	    h2(731) -> 732*
33.77/8.71	    h2(322) -> 323*
33.77/8.71	    g2(479) -> 480*
33.77/8.71	    g2(666) -> 667*
33.77/8.71	    g2(60) -> 61*
33.77/8.71	    g2(207) -> 208*
33.77/8.71	    g2(92) -> 93*
33.77/8.71	    g2(481) -> 482*
33.77/8.71	    g2(62) -> 63*
33.77/8.71	    g2(209) -> 210*
33.77/8.71	    g2(351) -> 352*
33.77/8.71	    g2(705) -> 706*
33.77/8.71	    g2(94) -> 95*
33.77/8.71	    g2(483) -> 484*
33.77/8.71	    g2(201) -> 202*
33.77/8.71	    g2(363) -> 364*
33.77/8.71	    g2(343) -> 344*
33.77/8.71	    g2(96) -> 97*
33.77/8.71	    g2(485) -> 486*
33.77/8.71	    g2(637) -> 638*
33.77/8.71	    g2(365) -> 366*
33.77/8.71	    g2(562) -> 563*
33.77/8.71	    g2(355) -> 356*
33.77/8.71	    g2(487) -> 488*
33.77/8.71	    g2(78) -> 79*
33.77/8.71	    g2(664) -> 665*
33.77/8.71	    g2(357) -> 358*
33.77/8.71	    active2(72) -> 73*
33.77/8.71	    active2(193) -> 194*
33.77/8.71	    active2(63) -> 64*
33.77/8.71	    active2(195) -> 196*
33.77/8.71	    d2() -> 55*
33.77/8.71	    mark2(41) -> 42*
33.77/8.71	    c2() -> 60*
33.77/8.71	    h3(474) -> 475*
33.77/8.71	    h3(464) -> 465*
33.77/8.71	    h3(621) -> 622*
33.77/8.71	    h3(187) -> 188*
33.77/8.71	    h3(546) -> 547*
33.77/8.71	    h3(733) -> 734*
33.77/8.71	    h3(314) -> 315*
33.77/8.71	    h3(304) -> 305*
33.77/8.71	    h3(466) -> 467*
33.77/8.71	    h3(229) -> 230*
33.77/8.71	    h3(623) -> 624*
33.77/8.71	    h3(725) -> 726*
33.77/8.71	    h3(124) -> 125*
33.77/8.71	    h3(306) -> 307*
33.77/8.71	    h3(468) -> 469*
33.77/8.71	    h3(660) -> 661*
33.77/8.71	    h3(236) -> 237*
33.77/8.71	    h3(428) -> 429*
33.77/8.71	    h3(625) -> 626*
33.77/8.71	    h3(181) -> 182*
33.77/8.71	    h3(560) -> 561*
33.77/8.71	    h3(727) -> 728*
33.77/8.71	    h3(308) -> 309*
33.77/8.71	    h3(697) -> 698*
33.77/8.71	    h3(470) -> 471*
33.77/8.71	    h3(238) -> 239*
33.77/8.71	    h3(617) -> 618*
33.77/8.71	    h3(552) -> 553*
33.77/8.71	    h3(542) -> 543*
33.77/8.71	    h3(310) -> 311*
33.77/8.71	    h3(472) -> 473*
33.77/8.71	    h3(462) -> 463*
33.77/8.71	    h3(432) -> 433*
33.77/8.71	    h3(619) -> 620*
33.77/8.71	    h3(554) -> 555*
33.77/8.71	    h3(544) -> 545*
33.77/8.71	    h3(312) -> 313*
33.77/8.71	    7 -> 21,11
33.77/8.71	    11 -> 67*
33.77/8.71	    12 -> 78,7,28
33.77/8.71	    13 -> 7*
33.77/8.71	    14 -> 12*
33.77/8.71	    19 -> 62,40,30
33.77/8.71	    20 -> 12*
33.77/8.71	    21 -> 49,43
33.77/8.71	    22 -> 94,7
33.77/8.71	    23 -> 7*
33.77/8.71	    28 -> 114,92,86
33.77/8.71	    29 -> 7*
33.77/8.71	    30 -> 108,96,84
33.77/8.71	    31 -> 7*
33.77/8.71	    40 -> 181*
33.77/8.71	    41 -> 229,201
33.77/8.71	    42 -> 163,196,170,176,64,13,31,23,29
33.77/8.71	    43 -> 189*
33.77/8.71	    44 -> 12*
33.77/8.71	    49 -> 187*
33.77/8.71	    50 -> 44,12,7,11,21,28,41
33.77/8.71	    55 -> 72,41
33.77/8.71	    60 -> 161*
33.77/8.71	    61 -> 41*
33.77/8.71	    62 -> 124*
33.77/8.71	    63 -> 238,209
33.77/8.71	    64 -> 13,7
33.77/8.71	    68 -> 63*
33.77/8.71	    72 -> 236,207
33.77/8.71	    73 -> 13,7
33.77/8.71	    78 -> 149,141
33.77/8.71	    79 -> 22,7
33.77/8.71	    84 -> 286,145
33.77/8.71	    85 -> 169,7
33.77/8.71	    86 -> 284,147
33.77/8.71	    87 -> 175,7
33.77/8.71	    92 -> 155,131
33.77/8.71	    93 -> 22,7
33.77/8.71	    94 -> 153,133
33.77/8.71	    95 -> 22,7
33.77/8.71	    96 -> 151,139
33.77/8.71	    97 -> 22,7
33.77/8.71	    108 -> 312*
33.77/8.71	    109 -> 188,190,68,50,44,63,193,12,7,11,21,28
33.77/8.71	    114 -> 306*
33.77/8.71	    115 -> 188,190,68,50,44,63,195,12,7,11,21,28
33.77/8.71	    124 -> 338*
33.77/8.71	    125 -> 418,343
33.77/8.71	    126 -> 299,301,64,13
33.77/8.71	    131 -> 322*
33.77/8.71	    132 -> 12*
33.77/8.71	    133 -> 318*
33.77/8.71	    134 -> 12*
33.77/8.71	    139 -> 330*
33.77/8.71	    140 -> 12*
33.77/8.71	    141 -> 324*
33.77/8.71	    142 -> 12*
33.77/8.71	    145 -> 316*
33.77/8.71	    146 -> 12*
33.77/8.71	    147 -> 332*
33.77/8.71	    148 -> 12*
33.77/8.71	    149 -> 304*
33.77/8.71	    150 -> 41*
33.77/8.71	    151 -> 308*
33.77/8.71	    152 -> 41*
33.77/8.71	    153 -> 310*
33.77/8.71	    154 -> 41*
33.77/8.71	    155 -> 314*
33.77/8.71	    156 -> 41*
33.77/8.71	    161 -> 259*
33.77/8.71	    162 -> 426,351
33.77/8.71	    163 -> 42,23,29,31
33.77/8.71	    169 -> 434,363
33.77/8.71	    170 -> 7*
33.77/8.71	    175 -> 440,365
33.77/8.71	    176 -> 7*
33.77/8.71	    182 -> 162*
33.77/8.71	    188 -> 162*
33.77/8.71	    190 -> 63*
33.77/8.71	    193 -> 428,355
33.77/8.71	    194 -> 13,7
33.77/8.71	    195 -> 432,357
33.77/8.71	    196 -> 13,7
33.77/8.71	    200 -> 162*
33.77/8.71	    201 -> 274*
33.77/8.71	    202 -> 22,7,21,11,43,67,94
33.77/8.71	    207 -> 266*
33.77/8.71	    208 -> 22,7,21,11,43,67,94
33.77/8.71	    209 -> 272*
33.77/8.71	    210 -> 22,7,21,11,43,67,94
33.77/8.71	    230 -> 188,190,162,298,68,50,44,12,7,28,86,114,41,63
33.77/8.71	    237 -> 188,190,162,300,68,50,44,12,7,28,86,114,41,63
33.77/8.71	    239 -> 188,190,162,302,68,50,44,12,7,28,86,114,41,63
33.77/8.71	    259 -> 476*
33.77/8.71	    260 -> 507,479
33.77/8.71	    261 -> 163,42,29,23,31,64
33.77/8.71	    266 -> 472*
33.77/8.71	    267 -> 41*
33.77/8.71	    272 -> 462*
33.77/8.71	    273 -> 41*
33.77/8.71	    274 -> 468*
33.77/8.71	    275 -> 41*
33.77/8.71	    284 -> 466*
33.77/8.71	    285 -> 41*
33.77/8.71	    286 -> 470*
33.77/8.71	    287 -> 41*
33.77/8.71	    296 -> 460*
33.77/8.71	    297 -> 125*
33.77/8.71	    298 -> 511,483
33.77/8.71	    299 -> 42*
33.77/8.71	    300 -> 513,485
33.77/8.71	    301 -> 42*
33.77/8.71	    302 -> 515,487
33.77/8.71	    303 -> 42*
33.77/8.71	    305 -> 162*
33.77/8.71	    307 -> 162*
33.77/8.71	    309 -> 162*
33.77/8.71	    311 -> 162*
33.77/8.71	    313 -> 162*
33.77/8.71	    315 -> 162*
33.77/8.71	    317 -> 63*
33.77/8.71	    319 -> 63*
33.77/8.71	    323 -> 63*
33.77/8.71	    325 -> 63*
33.77/8.71	    331 -> 63*
33.77/8.71	    333 -> 63*
33.77/8.71	    339 -> 509,481
33.77/8.71	    340 -> 126,64,13,7
33.77/8.71	    343 -> 450*
33.77/8.71	    344 -> 22,7,21,11,43,67,189,94,153
33.77/8.71	    351 -> 446*
33.77/8.71	    352 -> 22,7,21,11,43,67,189,94,153
33.77/8.71	    355 -> 454*
33.77/8.71	    356 -> 22,7,21,11,43,67,189,94,153
33.77/8.71	    357 -> 456*
33.77/8.71	    358 -> 22,7,21,11,43,67,189,94,153
33.77/8.71	    363 -> 448*
33.77/8.71	    364 -> 22,7,21,11,43,67,189,94,153
33.77/8.71	    365 -> 452*
33.77/8.71	    366 -> 22,7,21,11,43,67,189,94,153
33.77/8.71	    419 -> 188,68,50,190,162
33.77/8.71	    427 -> 188,68,50,190,162
33.77/8.71	    429 -> 188,68,50,190,162
33.77/8.71	    433 -> 188,68,50,190,162
33.77/8.71	    434 -> 464*
33.77/8.71	    435 -> 188,68,50,190,162
33.77/8.71	    440 -> 474*
33.77/8.71	    441 -> 188,68,50,190,162
33.77/8.71	    446 -> 546*
33.77/8.71	    447 -> 41*
33.77/8.71	    448 -> 552*
33.77/8.71	    449 -> 41*
33.77/8.71	    450 -> 554*
33.77/8.71	    451 -> 41*
33.77/8.71	    452 -> 560*
33.77/8.71	    453 -> 41*
33.77/8.71	    454 -> 542*
33.77/8.71	    455 -> 41*
33.77/8.71	    456 -> 544*
33.77/8.71	    457 -> 41*
33.77/8.71	    458 -> 540*
33.77/8.71	    459 -> 260*
33.77/8.71	    460 -> 517*
33.77/8.71	    461 -> 339*
33.77/8.71	    463 -> 162*
33.77/8.71	    465 -> 162*
33.77/8.71	    467 -> 162*
33.77/8.71	    469 -> 162*
33.77/8.71	    471 -> 162*
33.77/8.71	    473 -> 162*
33.77/8.71	    475 -> 162*
33.77/8.71	    477 -> 583,562
33.77/8.71	    478 -> 261,42
33.77/8.71	    479 -> 538,520
33.77/8.71	    480 -> 22,7,21,11,43,67,189,94,153,318
33.77/8.71	    481 -> 536,522
33.77/8.71	    482 -> 22,7,21,11,43,67,189,94,153,318
33.77/8.71	    483 -> 534,524
33.77/8.71	    484 -> 22,7,21,11,43,67,189,94,153,318
33.77/8.71	    485 -> 532,526
33.77/8.71	    486 -> 22,7,21,11,43,67,189,94,153,318
33.77/8.71	    487 -> 530,528
33.77/8.71	    488 -> 22,7,21,11,43,67,189,94,153,318
33.77/8.71	    508 -> 188,68,50,41,44,201,274,190,162,426
33.77/8.71	    510 -> 188,68,50,41,44,201,274,190,162,426
33.77/8.71	    512 -> 188,68,50,41,44,201,274,190,162,426
33.77/8.71	    514 -> 188,68,50,41,44,201,274,190,162,426
33.77/8.71	    516 -> 188,68,50,41,44,201,274,190,162,426
33.77/8.71	    517 -> 614*
33.77/8.71	    518 -> 647,637
33.77/8.71	    519 -> 340,126,301,163
33.77/8.71	    520 -> 631*
33.77/8.71	    521 -> 12*
33.77/8.71	    522 -> 629*
33.77/8.71	    523 -> 12*
33.77/8.71	    524 -> 627*
33.77/8.71	    525 -> 12*
33.77/8.71	    526 -> 635*
33.77/8.71	    527 -> 12*
33.77/8.71	    528 -> 633*
33.77/8.71	    529 -> 12*
33.77/8.71	    530 -> 621*
33.77/8.71	    531 -> 41*
33.77/8.71	    532 -> 623*
33.77/8.71	    533 -> 41*
33.77/8.71	    534 -> 625*
33.77/8.71	    535 -> 41*
33.77/8.71	    536 -> 617*
33.77/8.71	    537 -> 41*
33.77/8.71	    538 -> 619*
33.77/8.71	    539 -> 41*
33.77/8.71	    540 -> 605*
33.77/8.71	    541 -> 477*
33.77/8.71	    543 -> 162*
33.77/8.71	    545 -> 162*
33.77/8.71	    547 -> 162*
33.77/8.71	    553 -> 162*
33.77/8.71	    555 -> 162*
33.77/8.71	    561 -> 162*
33.77/8.71	    562 -> 612,608
33.77/8.71	    563 -> 22,7,21,11,43,67,189,94,153,318
33.77/8.71	    584 -> 188,162,190,50,44,12,78,149,92,306,155,284,324,332,322,41,229,468,68,351,446
33.77/8.71	    605 -> 653*
33.77/8.71	    606 -> 668,664
33.77/8.71	    607 -> 478,261
33.77/8.71	    608 -> 662*
33.77/8.71	    609 -> 12*
33.77/8.71	    612 -> 660*
33.77/8.71	    613 -> 41*
33.77/8.71	    615 -> 670,666
33.77/8.71	    616 -> 519,340
33.77/8.71	    618 -> 162*
33.77/8.71	    620 -> 162*
33.77/8.71	    622 -> 162*
33.77/8.71	    624 -> 162*
33.77/8.71	    626 -> 162*
33.77/8.71	    628 -> 63*
33.77/8.71	    630 -> 63*
33.77/8.71	    632 -> 63*
33.77/8.71	    634 -> 63*
33.77/8.71	    636 -> 63*
33.77/8.71	    637 -> 651,649
33.77/8.71	    638 -> 22,7,21,11,43,67,189,94,153,318
33.77/8.71	    648 -> 188,68,50,190,162,426,546
33.77/8.71	    649 -> 703*
33.77/8.71	    650 -> 12*
33.77/8.71	    651 -> 697*
33.77/8.71	    652 -> 41*
33.77/8.71	    654 -> 719,705
33.77/8.71	    655 -> 607,478
33.77/8.71	    661 -> 162*
33.77/8.71	    663 -> 63*
33.77/8.71	    664 -> 689,687
33.77/8.71	    665 -> 22,7,21,11,43,67,189,94,153,318
33.77/8.71	    666 -> 695,681
33.77/8.71	    667 -> 22,7,21,11,43,67,189,94,153,318
33.77/8.71	    669 -> 188,68,50,190,162,426,546
33.77/8.71	    671 -> 188,68,50,190,162,426,546
33.77/8.71	    681 -> 729*
33.77/8.71	    682 -> 12*
33.77/8.71	    687 -> 731*
33.77/8.71	    688 -> 12*
33.77/8.71	    689 -> 727*
33.77/8.71	    690 -> 41*
33.77/8.71	    695 -> 725*
33.77/8.71	    696 -> 41*
33.77/8.71	    698 -> 162*
33.77/8.71	    704 -> 63*
33.77/8.71	    705 -> 723,721
33.77/8.71	    706 -> 22,7,21,11,43,67,189,94,153,318
33.77/8.71	    720 -> 188,68,50,190,162,426,546
33.77/8.71	    721 -> 735*
33.77/8.71	    722 -> 12*
33.77/8.71	    723 -> 733*
33.77/8.71	    724 -> 41*
33.77/8.71	    726 -> 162*
33.77/8.71	    728 -> 162*
33.77/8.71	    730 -> 63*
33.77/8.71	    732 -> 63*
33.77/8.71	    734 -> 162*
33.77/8.71	    736 -> 63*
33.77/8.71	  problem:
33.77/8.71	   
33.77/8.71	  Qed
33.77/8.72	EOF