YES(?,O(n^1))

Problem:
 t(o(x1)) -> m(a(x1))
 t(e(x1)) -> n(s(x1))
 a(l(x1)) -> a(t(x1))
 o(m(a(x1))) -> t(e(n(x1)))
 s(a(x1)) -> l(a(t(o(m(a(t(e(x1))))))))
 n(s(x1)) -> a(l(a(t(x1))))

Proof:
 Bounds Processor:
  bound: 8
  enrichment: match
  automaton:
   final states: {9}
   transitions:
    l3(299) -> 300*
    l3(234) -> 235*
    l3(229) -> 230*
    l3(204) -> 205*
    t3(297) -> 298*
    t3(232) -> 233*
    t3(227) -> 228*
    t3(202) -> 203*
    t3(528) -> 529*
    t3(580) -> 581*
    t3(293) -> 294*
    t3(198) -> 199*
    t3(163) -> 164*
    t3(360) -> 361*
    t3(447) -> 448*
    t3(195) -> 196*
    t3(534) -> 535*
    o3(296) -> 297*
    o3(201) -> 202*
    m3(134) -> 135*
    m3(295) -> 296*
    m3(200) -> 201*
    e3(292) -> 293*
    e3(429) -> 430*
    e3(197) -> 198*
    e3(314) -> 315*
    e3(194) -> 195*
    n3(161) -> 162*
    n3(141) -> 142*
    n3(193) -> 194*
    s3(476) -> 477*
    s3(254) -> 255*
    s3(381) -> 382*
    s3(383) -> 384*
    s3(160) -> 161*
    s3(140) -> 141*
    a4(237) -> 238*
    a4(354) -> 355*
    a4(349) -> 350*
    a4(366) -> 367*
    a4(336) -> 337*
    a4(263) -> 264*
    a4(270) -> 271*
    a4(352) -> 353*
    a4(347) -> 348*
    a4(332) -> 333*
    l4(353) -> 354*
    l4(348) -> 349*
    l4(337) -> 338*
    t0(9) -> 9*
    t4(262) -> 263*
    t4(526) -> 527*
    t4(269) -> 270*
    t4(578) -> 579*
    t4(351) -> 352*
    t4(346) -> 347*
    t4(331) -> 332*
    t4(286) -> 287*
    t4(418) -> 419*
    t4(520) -> 521*
    t4(445) -> 446*
    t4(335) -> 336*
    o0(9) -> 9*
    o4(334) -> 335*
    m0(9) -> 9*
    m4(333) -> 334*
    m4(238) -> 239*
    m4(367) -> 368*
    a0(9) -> 9*
    e4(330) -> 331*
    e4(285) -> 286*
    e4(417) -> 418*
    e0(9) -> 9*
    n4(252) -> 253*
    n4(284) -> 285*
    n4(244) -> 245*
    n4(416) -> 417*
    n4(390) -> 391*
    n0(9) -> 9*
    s4(389) -> 390*
    s4(379) -> 380*
    s4(251) -> 252*
    s4(465) -> 466*
    s4(243) -> 244*
    s0(9) -> 9*
    a5(399) -> 400*
    a5(516) -> 517*
    a5(441) -> 442*
    a5(436) -> 437*
    a5(518) -> 519*
    a5(443) -> 444*
    a5(438) -> 439*
    a5(373) -> 374*
    a5(405) -> 406*
    l0(9) -> 9*
    l5(517) -> 518*
    l5(442) -> 443*
    l5(437) -> 438*
    a1(40) -> 41*
    a1(24) -> 25*
    a1(36) -> 37*
    a1(13) -> 14*
    t5(404) -> 405*
    t5(506) -> 507*
    t5(398) -> 399*
    t5(515) -> 516*
    t5(440) -> 441*
    t5(435) -> 436*
    t5(572) -> 573*
    t5(427) -> 428*
    l1(41) -> 42*
    l1(43) -> 44*
    e5(426) -> 427*
    t1(35) -> 36*
    t1(74) -> 75*
    t1(39) -> 40*
    t1(28) -> 29*
    t1(23) -> 24*
    n5(396) -> 397*
    n5(463) -> 464*
    n5(425) -> 426*
    n5(377) -> 378*
    o1(38) -> 39*
    s5(376) -> 377*
    s5(395) -> 396*
    s5(462) -> 463*
    m1(37) -> 38*
    m1(14) -> 15*
    m5(374) -> 375*
    e1(431) -> 432*
    e1(27) -> 28*
    e1(214) -> 215*
    e1(316) -> 317*
    e1(104) -> 105*
    e1(34) -> 35*
    e1(322) -> 323*
    a6(504) -> 505*
    a6(499) -> 500*
    a6(568) -> 569*
    a6(483) -> 484*
    a6(570) -> 571*
    a6(490) -> 491*
    a6(552) -> 553*
    a6(502) -> 503*
    a6(497) -> 498*
    n1(282) -> 283*
    n1(17) -> 18*
    n1(94) -> 95*
    n1(276) -> 277*
    n1(186) -> 187*
    n1(26) -> 27*
    n1(420) -> 421*
    n1(188) -> 189*
    n1(88) -> 89*
    l6(503) -> 504*
    l6(498) -> 499*
    l6(569) -> 570*
    s1(16) -> 17*
    t6(489) -> 490*
    t6(551) -> 552*
    t6(501) -> 502*
    t6(496) -> 497*
    t6(567) -> 568*
    t6(482) -> 483*
    a2(112) -> 113*
    a2(49) -> 50*
    a2(81) -> 82*
    a2(108) -> 109*
    a2(68) -> 69*
    a2(120) -> 121*
    n6(454) -> 455*
    l2(121) -> 122*
    l2(113) -> 114*
    s6(453) -> 454*
    t2(80) -> 81*
    t2(107) -> 108*
    t2(67) -> 68*
    t2(119) -> 120*
    t2(111) -> 112*
    t2(98) -> 99*
    a7(541) -> 542*
    a7(593) -> 594*
    a7(558) -> 559*
    a7(560) -> 561*
    a7(549) -> 550*
    o2(110) -> 111*
    l7(559) -> 560*
    m2(50) -> 51*
    m2(109) -> 110*
    t7(548) -> 549*
    t7(540) -> 541*
    t7(592) -> 593*
    t7(557) -> 558*
    e2(324) -> 325*
    e2(97) -> 98*
    e2(433) -> 434*
    e2(216) -> 217*
    e2(328) -> 329*
    e2(106) -> 107*
    a8(588) -> 589*
    n2(65) -> 66*
    n2(96) -> 97*
    n2(58) -> 59*
    t8(587) -> 588*
    s2(147) -> 148*
    s2(57) -> 58*
    s2(478) -> 479*
    s2(64) -> 65*
    s2(256) -> 257*
    s2(385) -> 386*
    s2(387) -> 388*
    a3(294) -> 295*
    a3(199) -> 200*
    a3(164) -> 165*
    a3(298) -> 299*
    a3(233) -> 234*
    a3(228) -> 229*
    a3(203) -> 204*
    a3(133) -> 134*
    a3(235) -> 236*
    a3(230) -> 231*
    9 -> 34,26,23,16,13
    13 -> 88*
    15 -> 228,120,24,9
    16 -> 119*
    18 -> 228,120,24,9
    24 -> 106,104,94
    25 -> 89,27,14,43,9
    27 -> 57*
    29 -> 9*
    34 -> 64*
    36 -> 96*
    38 -> 49*
    41 -> 80,74
    42 -> 65,17,9
    43 -> 67*
    44 -> 24*
    51 -> 40*
    57 -> 232*
    59 -> 29*
    64 -> 227*
    66 -> 36*
    68 -> 216,214,197,188
    69 -> 18,25,9,43
    75 -> 24*
    81 -> 186*
    82 -> 14*
    89 -> 27*
    95 -> 27*
    97 -> 140*
    99 -> 39*
    104 -> 147*
    105 -> 35*
    106 -> 160*
    108 -> 193*
    110 -> 133*
    114 -> 58,65,17
    121 -> 163*
    122 -> 68*
    135 -> 112*
    140 -> 351*
    142 -> 99,39
    147 -> 360*
    148 -> 65*
    160 -> 346*
    162 -> 108*
    164 -> 330,324,316,292,276
    165 -> 69,25,43,14,27,67,18,94,106
    187 -> 27*
    189 -> 27*
    194 -> 251*
    196 -> 111*
    197 -> 243*
    199 -> 284*
    201 -> 237*
    205 -> 161,148,58,65
    214 -> 256*
    215 -> 35*
    216 -> 254*
    217 -> 107*
    229 -> 269*
    231 -> 66,36,96
    234 -> 262*
    235 -> 328,322,314,282
    236 -> 59*
    239 -> 203*
    243 -> 440*
    245 -> 199*
    251 -> 435*
    253 -> 196,111
    254 -> 445*
    255 -> 161*
    256 -> 447*
    257 -> 65*
    263 -> 433,431,429,420
    264 -> 236,59,29
    271 -> 231*
    277 -> 27*
    283 -> 27*
    285 -> 376*
    287 -> 202*
    292 -> 389*
    294 -> 416*
    296 -> 366*
    300 -> 58,148
    314 -> 379*
    315 -> 198*
    316 -> 385*
    317 -> 35*
    322 -> 387*
    323 -> 35*
    324 -> 381*
    325 -> 107*
    328 -> 383*
    329 -> 107*
    330 -> 395*
    332 -> 425*
    334 -> 373*
    338 -> 161*
    348 -> 404*
    350 -> 162,108,193
    353 -> 398*
    355 -> 142*
    361 -> 228*
    368 -> 298*
    375 -> 336*
    376 -> 501*
    378 -> 287*
    379 -> 506*
    380 -> 244*
    381 -> 520*
    382 -> 161*
    383 -> 526*
    384 -> 161*
    385 -> 528*
    386 -> 65*
    387 -> 534*
    388 -> 65*
    389 -> 515*
    391 -> 294*
    395 -> 496*
    397 -> 332*
    400 -> 355,142,99
    406 -> 350,162
    417 -> 462*
    419 -> 297*
    421 -> 27*
    426 -> 453*
    428 -> 335*
    429 -> 465*
    430 -> 198*
    431 -> 478*
    432 -> 35*
    433 -> 476*
    434 -> 107*
    437 -> 489*
    439 -> 253,196
    442 -> 482*
    444 -> 245*
    446 -> 347*
    448 -> 228*
    453 -> 557*
    455 -> 428,335
    462 -> 567*
    464 -> 419,297
    465 -> 572*
    466 -> 244*
    476 -> 578*
    477 -> 161*
    478 -> 580*
    479 -> 65*
    484 -> 444,245,284
    491 -> 439,253,196,111
    498 -> 548*
    500 -> 397,332,425
    503 -> 540*
    505 -> 378*
    507 -> 441*
    517 -> 551*
    519 -> 391*
    521 -> 347*
    527 -> 347*
    529 -> 228*
    535 -> 228*
    542 -> 505,378,202
    550 -> 500,397
    553 -> 519,391,416
    559 -> 587*
    561 -> 455,428
    569 -> 592*
    571 -> 464*
    573 -> 441*
    579 -> 347*
    581 -> 228*
    589 -> 561,455,428,335
    594 -> 571,464,419
  problem:
   
  Qed