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:
 RT Transformation Processor:
  strict:
   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))))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [l](x0) = x0 + 13,
    
    [n](x0) = x0 + 10,
    
    [s](x0) = x0 + 5,
    
    [e](x0) = x0 + 4,
    
    [m](x0) = x0 + 19,
    
    [a](x0) = x0,
    
    [t](x0) = x0 + 1,
    
    [o](x0) = x0
   orientation:
    t(o(x1)) = x1 + 1 >= x1 + 19 = m(a(x1))
    
    t(e(x1)) = x1 + 5 >= x1 + 15 = n(s(x1))
    
    a(l(x1)) = x1 + 13 >= x1 + 1 = a(t(x1))
    
    o(m(a(x1))) = x1 + 19 >= x1 + 15 = t(e(n(x1)))
    
    s(a(x1)) = x1 + 5 >= x1 + 38 = l(a(t(o(m(a(t(e(x1))))))))
    
    n(s(x1)) = x1 + 15 >= x1 + 14 = a(l(a(t(x1))))
   problem:
    strict:
     t(o(x1)) -> m(a(x1))
     t(e(x1)) -> n(s(x1))
     s(a(x1)) -> l(a(t(o(m(a(t(e(x1))))))))
    weak:
     a(l(x1)) -> a(t(x1))
     o(m(a(x1))) -> t(e(n(x1)))
     n(s(x1)) -> a(l(a(t(x1))))
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [l](x0) = x0 + 2,
     
     [n](x0) = x0 + 26,
     
     [s](x0) = x0 + 5,
     
     [e](x0) = x0 + 5,
     
     [m](x0) = x0 + 16,
     
     [a](x0) = x0,
     
     [t](x0) = x0 + 1,
     
     [o](x0) = x0 + 16
    orientation:
     t(o(x1)) = x1 + 17 >= x1 + 16 = m(a(x1))
     
     t(e(x1)) = x1 + 6 >= x1 + 31 = n(s(x1))
     
     s(a(x1)) = x1 + 5 >= x1 + 41 = l(a(t(o(m(a(t(e(x1))))))))
     
     a(l(x1)) = x1 + 2 >= x1 + 1 = a(t(x1))
     
     o(m(a(x1))) = x1 + 32 >= x1 + 32 = t(e(n(x1)))
     
     n(s(x1)) = x1 + 31 >= x1 + 3 = a(l(a(t(x1))))
    problem:
     strict:
      t(e(x1)) -> n(s(x1))
      s(a(x1)) -> l(a(t(o(m(a(t(e(x1))))))))
     weak:
      t(o(x1)) -> m(a(x1))
      a(l(x1)) -> a(t(x1))
      o(m(a(x1))) -> t(e(n(x1)))
      n(s(x1)) -> a(l(a(t(x1))))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [l](x0) = x0,
      
      [n](x0) = x0 + 5,
      
      [s](x0) = x0 + 3,
      
      [e](x0) = x0 + 15,
      
      [m](x0) = x0 + 6,
      
      [a](x0) = x0 + 4,
      
      [t](x0) = x0,
      
      [o](x0) = x0 + 10
     orientation:
      t(e(x1)) = x1 + 15 >= x1 + 8 = n(s(x1))
      
      s(a(x1)) = x1 + 7 >= x1 + 39 = l(a(t(o(m(a(t(e(x1))))))))
      
      t(o(x1)) = x1 + 10 >= x1 + 10 = m(a(x1))
      
      a(l(x1)) = x1 + 4 >= x1 + 4 = a(t(x1))
      
      o(m(a(x1))) = x1 + 20 >= x1 + 20 = t(e(n(x1)))
      
      n(s(x1)) = x1 + 8 >= x1 + 8 = a(l(a(t(x1))))
     problem:
      strict:
       s(a(x1)) -> l(a(t(o(m(a(t(e(x1))))))))
      weak:
       t(e(x1)) -> n(s(x1))
       t(o(x1)) -> m(a(x1))
       a(l(x1)) -> a(t(x1))
       o(m(a(x1))) -> t(e(n(x1)))
       n(s(x1)) -> a(l(a(t(x1))))
     Bounds Processor:
      bound: 3
      enrichment: match-rt
      automaton:
       final states: {9}
       transitions:
        a3(179) -> 180*
        a3(181) -> 182*
        a3(153) -> 154*
        a3(155) -> 156*
        l1(26) -> 27*
        l1(68) -> 69*
        l3(154) -> 155*
        l3(180) -> 181*
        a1(35) -> 36*
        a1(25) -> 26*
        a1(67) -> 68*
        a1(91) -> 92*
        a1(21) -> 22*
        a1(43) -> 44*
        t3(172) -> 173*
        t3(152) -> 153*
        t3(223) -> 224*
        t3(213) -> 214*
        t3(178) -> 179*
        t1(20) -> 21*
        t1(42) -> 43*
        t1(64) -> 65*
        t1(24) -> 25*
        t1(101) -> 102*
        t1(66) -> 67*
        t1(105) -> 106*
        o1(23) -> 24*
        m1(92) -> 93*
        m1(22) -> 23*
        m1(36) -> 37*
        e1(104) -> 105*
        e1(19) -> 20*
        e1(191) -> 192*
        e1(63) -> 64*
        e1(58) -> 59*
        n1(62) -> 63*
        n1(29) -> 30*
        n1(221) -> 222*
        n1(103) -> 104*
        n1(78) -> 79*
        n1(135) -> 136*
        s1(75) -> 76*
        s1(77) -> 78*
        s1(134) -> 135*
        s1(206) -> 207*
        s1(28) -> 29*
        l2(52) -> 53*
        l2(113) -> 114*
        l2(185) -> 186*
        l2(165) -> 166*
        s0(9) -> 9*
        a2(112) -> 113*
        a2(47) -> 48*
        a2(184) -> 185*
        a2(164) -> 165*
        a2(114) -> 115*
        a2(94) -> 95*
        a2(186) -> 187*
        a2(166) -> 167*
        a2(51) -> 52*
        a0(9) -> 9*
        t2(50) -> 51*
        t2(174) -> 175*
        t2(109) -> 110*
        t2(161) -> 162*
        t2(111) -> 112*
        t2(46) -> 47*
        t2(183) -> 184*
        t2(163) -> 164*
        t2(148) -> 149*
        t2(230) -> 231*
        t2(215) -> 216*
        l0(9) -> 9*
        o2(49) -> 50*
        t0(9) -> 9*
        m2(95) -> 96*
        m2(48) -> 49*
        o0(9) -> 9*
        e2(45) -> 46*
        e2(193) -> 194*
        e2(108) -> 109*
        m0(9) -> 9*
        n2(85) -> 86*
        n2(132) -> 133*
        n2(107) -> 108*
        e0(9) -> 9*
        s2(204) -> 205*
        s2(84) -> 85*
        s2(131) -> 132*
        n0(9) -> 9*
        9 -> 91,66,19
        19 -> 28*
        21 -> 62*
        23 -> 35*
        26 -> 42*
        27 -> 29,9
        28 -> 111*
        30 -> 112,67,21
        37 -> 25*
        43 -> 103,58,45
        44 -> 92,9,19
        45 -> 84*
        47 -> 107*
        49 -> 94*
        53 -> 29*
        58 -> 75*
        59 -> 20*
        63 -> 77*
        65 -> 24*
        68 -> 92,101
        69 -> 43*
        75 -> 161*
        76 -> 29*
        77 -> 163*
        79 -> 65*
        84 -> 152*
        86 -> 47*
        93 -> 112,67
        96 -> 51*
        102 -> 43*
        104 -> 134*
        106 -> 9*
        108 -> 131*
        110 -> 50*
        113 -> 148*
        115 -> 30,21,62
        131 -> 178*
        133 -> 110,50
        134 -> 183*
        136 -> 106,9
        149 -> 114*
        154 -> 172*
        156 -> 86,47,107
        162 -> 112*
        165 -> 174*
        167 -> 79*
        173 -> 155*
        175 -> 166*
        180 -> 213*
        182 -> 133,110
        185 -> 215*
        186 -> 221,193,191
        187 -> 136,106
        191 -> 206*
        192 -> 20*
        193 -> 204*
        194 -> 46*
        204 -> 223*
        205 -> 85*
        206 -> 230*
        207 -> 29*
        214 -> 181*
        216 -> 186*
        222 -> 104*
        224 -> 153*
        231 -> 112*
      problem:
       strict:
        
       weak:
        s(a(x1)) -> l(a(t(o(m(a(t(e(x1))))))))
        t(e(x1)) -> n(s(x1))
        t(o(x1)) -> m(a(x1))
        a(l(x1)) -> a(t(x1))
        o(m(a(x1))) -> t(e(n(x1)))
        n(s(x1)) -> a(l(a(t(x1))))
      Qed