MAYBE

Problem:
 r1(a(x1)) -> a(a(a(r1(x1))))
 r2(a(x1)) -> a(a(a(r2(x1))))
 a(l1(x1)) -> l1(a(a(a(x1))))
 a(a(l2(x1))) -> l2(a(a(x1)))
 r1(b(x1)) -> l1(b(x1))
 r2(b(x1)) -> l2(a(b(x1)))
 b(l1(x1)) -> b(r2(x1))
 b(l2(x1)) -> b(r1(x1))
 a(a(x1)) -> x1

Proof:
 Complexity Transformation Processor:
  strict:
   r1(a(x1)) -> a(a(a(r1(x1))))
   r2(a(x1)) -> a(a(a(r2(x1))))
   a(l1(x1)) -> l1(a(a(a(x1))))
   a(a(l2(x1))) -> l2(a(a(x1)))
   r1(b(x1)) -> l1(b(x1))
   r2(b(x1)) -> l2(a(b(x1)))
   b(l1(x1)) -> b(r2(x1))
   b(l2(x1)) -> b(r1(x1))
   a(a(x1)) -> x1
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [b](x0) = x0,
     
     [l2](x0) = x0 + 1,
     
     [l1](x0) = x0,
     
     [r2](x0) = x0,
     
     [r1](x0) = x0,
     
     [a](x0) = x0
    orientation:
     r1(a(x1)) = x1 >= x1 = a(a(a(r1(x1))))
     
     r2(a(x1)) = x1 >= x1 = a(a(a(r2(x1))))
     
     a(l1(x1)) = x1 >= x1 = l1(a(a(a(x1))))
     
     a(a(l2(x1))) = x1 + 1 >= x1 + 1 = l2(a(a(x1)))
     
     r1(b(x1)) = x1 >= x1 = l1(b(x1))
     
     r2(b(x1)) = x1 >= x1 + 1 = l2(a(b(x1)))
     
     b(l1(x1)) = x1 >= x1 = b(r2(x1))
     
     b(l2(x1)) = x1 + 1 >= x1 = b(r1(x1))
     
     a(a(x1)) = x1 >= x1 = x1
    problem:
     strict:
      r1(a(x1)) -> a(a(a(r1(x1))))
      r2(a(x1)) -> a(a(a(r2(x1))))
      a(l1(x1)) -> l1(a(a(a(x1))))
      a(a(l2(x1))) -> l2(a(a(x1)))
      r1(b(x1)) -> l1(b(x1))
      r2(b(x1)) -> l2(a(b(x1)))
      b(l1(x1)) -> b(r2(x1))
      a(a(x1)) -> x1
     weak:
      b(l2(x1)) -> b(r1(x1))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [b](x0) = x0,
       
       [l2](x0) = x0,
       
       [l1](x0) = x0 + 1,
       
       [r2](x0) = x0,
       
       [r1](x0) = x0,
       
       [a](x0) = x0
      orientation:
       r1(a(x1)) = x1 >= x1 = a(a(a(r1(x1))))
       
       r2(a(x1)) = x1 >= x1 = a(a(a(r2(x1))))
       
       a(l1(x1)) = x1 + 1 >= x1 + 1 = l1(a(a(a(x1))))
       
       a(a(l2(x1))) = x1 >= x1 = l2(a(a(x1)))
       
       r1(b(x1)) = x1 >= x1 + 1 = l1(b(x1))
       
       r2(b(x1)) = x1 >= x1 = l2(a(b(x1)))
       
       b(l1(x1)) = x1 + 1 >= x1 = b(r2(x1))
       
       a(a(x1)) = x1 >= x1 = x1
       
       b(l2(x1)) = x1 >= x1 = b(r1(x1))
      problem:
       strict:
        r1(a(x1)) -> a(a(a(r1(x1))))
        r2(a(x1)) -> a(a(a(r2(x1))))
        a(l1(x1)) -> l1(a(a(a(x1))))
        a(a(l2(x1))) -> l2(a(a(x1)))
        r1(b(x1)) -> l1(b(x1))
        r2(b(x1)) -> l2(a(b(x1)))
        a(a(x1)) -> x1
       weak:
        b(l1(x1)) -> b(r2(x1))
        b(l2(x1)) -> b(r1(x1))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [b](x0) = x0,
         
         [l2](x0) = x0,
         
         [l1](x0) = x0,
         
         [r2](x0) = x0,
         
         [r1](x0) = x0,
         
         [a](x0) = x0 + 1
        orientation:
         r1(a(x1)) = x1 + 1 >= x1 + 3 = a(a(a(r1(x1))))
         
         r2(a(x1)) = x1 + 1 >= x1 + 3 = a(a(a(r2(x1))))
         
         a(l1(x1)) = x1 + 1 >= x1 + 3 = l1(a(a(a(x1))))
         
         a(a(l2(x1))) = x1 + 2 >= x1 + 2 = l2(a(a(x1)))
         
         r1(b(x1)) = x1 >= x1 = l1(b(x1))
         
         r2(b(x1)) = x1 >= x1 + 1 = l2(a(b(x1)))
         
         a(a(x1)) = x1 + 2 >= x1 = x1
         
         b(l1(x1)) = x1 >= x1 = b(r2(x1))
         
         b(l2(x1)) = x1 >= x1 = b(r1(x1))
        problem:
         strict:
          r1(a(x1)) -> a(a(a(r1(x1))))
          r2(a(x1)) -> a(a(a(r2(x1))))
          a(l1(x1)) -> l1(a(a(a(x1))))
          a(a(l2(x1))) -> l2(a(a(x1)))
          r1(b(x1)) -> l1(b(x1))
          r2(b(x1)) -> l2(a(b(x1)))
         weak:
          a(a(x1)) -> x1
          b(l1(x1)) -> b(r2(x1))
          b(l2(x1)) -> b(r1(x1))
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [b](x0) = x0,
           
           [l2](x0) = x0,
           
           [l1](x0) = x0 + 1,
           
           [r2](x0) = x0 + 1,
           
           [r1](x0) = x0,
           
           [a](x0) = x0
          orientation:
           r1(a(x1)) = x1 >= x1 = a(a(a(r1(x1))))
           
           r2(a(x1)) = x1 + 1 >= x1 + 1 = a(a(a(r2(x1))))
           
           a(l1(x1)) = x1 + 1 >= x1 + 1 = l1(a(a(a(x1))))
           
           a(a(l2(x1))) = x1 >= x1 = l2(a(a(x1)))
           
           r1(b(x1)) = x1 >= x1 + 1 = l1(b(x1))
           
           r2(b(x1)) = x1 + 1 >= x1 = l2(a(b(x1)))
           
           a(a(x1)) = x1 >= x1 = x1
           
           b(l1(x1)) = x1 + 1 >= x1 + 1 = b(r2(x1))
           
           b(l2(x1)) = x1 >= x1 = b(r1(x1))
          problem:
           strict:
            r1(a(x1)) -> a(a(a(r1(x1))))
            r2(a(x1)) -> a(a(a(r2(x1))))
            a(l1(x1)) -> l1(a(a(a(x1))))
            a(a(l2(x1))) -> l2(a(a(x1)))
            r1(b(x1)) -> l1(b(x1))
           weak:
            r2(b(x1)) -> l2(a(b(x1)))
            a(a(x1)) -> x1
            b(l1(x1)) -> b(r2(x1))
            b(l2(x1)) -> b(r1(x1))
          Bounds Processor:
           bound: 0
           enrichment: match
           automaton:
            final states: {6,5,4,3}
            transitions:
             r10(2) -> 3*
             r10(1) -> 3*
             a0(50) -> 51*
             a0(25) -> 26*
             a0(2) -> 5*
             a0(144) -> 145*
             a0(49) -> 50*
             a0(24) -> 25*
             a0(1) -> 5*
             a0(118) -> 119*
             a0(48) -> 49*
             r20(2) -> 4*
             r20(1) -> 4*
             l10(2) -> 1*
             l10(51) -> 52*
             l10(26) -> 27*
             l10(1) -> 1*
             l20(2) -> 2*
             l20(79) -> 80*
             l20(1) -> 2*
             b0(2) -> 6*
             b0(46) -> 47*
             b0(1) -> 6*
             b0(28) -> 29*
             1 -> 25*
             2 -> 25*
             3 -> 46*
             4 -> 28*
             5 -> 24*
             24 -> 145,26
             25 -> 49,79
             26 -> 48*
             27 -> 145,119,5
             29 -> 6*
             47 -> 6*
             48 -> 50*
             49 -> 51*
             50 -> 119*
             51 -> 118*
             52 -> 49,25
             79 -> 144*
             80 -> 49,25
             118 -> 25,49
             119 -> 24*
             144 -> 25,49
             145 -> 24*
           problem:
            strict:
             r1(a(x1)) -> a(a(a(r1(x1))))
             r2(a(x1)) -> a(a(a(r2(x1))))
             a(l1(x1)) -> l1(a(a(a(x1))))
             a(a(l2(x1))) -> l2(a(a(x1)))
            weak:
             r1(b(x1)) -> l1(b(x1))
             r2(b(x1)) -> l2(a(b(x1)))
             a(a(x1)) -> x1
             b(l1(x1)) -> b(r2(x1))
             b(l2(x1)) -> b(r1(x1))
           Bounds Processor:
            bound: 0
            enrichment: match
            automaton:
             final states: {6,5,4,3}
             transitions:
              r10(2) -> 3*
              r10(1) -> 3*
              a0(50) -> 51*
              a0(132) -> 133*
              a0(92) -> 93*
              a0(52) -> 53*
              a0(7) -> 8*
              a0(2) -> 5*
              a0(51) -> 52*
              a0(1) -> 5*
              a0(8) -> 9*
              r20(2) -> 4*
              r20(1) -> 4*
              l10(2) -> 1*
              l10(9) -> 10*
              l10(1) -> 1*
              l10(53) -> 54*
              l20(55) -> 56*
              l20(2) -> 2*
              l20(1) -> 2*
              b0(32) -> 33*
              b0(2) -> 6*
              b0(34) -> 35*
              b0(1) -> 6*
              1 -> 51,8
              2 -> 51,8
              3 -> 34*
              4 -> 32*
              5 -> 7*
              7 -> 133,9
              8 -> 51,55
              9 -> 50*
              10 -> 93,133,5
              33 -> 6*
              35 -> 6*
              50 -> 93,52
              51 -> 53*
              52 -> 93*
              53 -> 92*
              54 -> 51,8
              55 -> 132*
              56 -> 51,8
              92 -> 8,53
              93 -> 7*
              132 -> 8,53
              133 -> 7*
            problem:
             strict:
              r2(a(x1)) -> a(a(a(r2(x1))))
              a(l1(x1)) -> l1(a(a(a(x1))))
              a(a(l2(x1))) -> l2(a(a(x1)))
             weak:
              r1(a(x1)) -> a(a(a(r1(x1))))
              r1(b(x1)) -> l1(b(x1))
              r2(b(x1)) -> l2(a(b(x1)))
              a(a(x1)) -> x1
              b(l1(x1)) -> b(r2(x1))
              b(l2(x1)) -> b(r1(x1))
            Bounds Processor:
             bound: 0
             enrichment: match
             automaton:
              final states: {6,5,4,3}
              transitions:
               r10(2) -> 5*
               r10(1) -> 5*
               a0(77) -> 78*
               a0(37) -> 38*
               a0(7) -> 8*
               a0(2) -> 4*
               a0(39) -> 40*
               a0(111) -> 112*
               a0(1) -> 4*
               a0(38) -> 39*
               a0(8) -> 9*
               r20(2) -> 3*
               r20(1) -> 3*
               l10(40) -> 41*
               l10(2) -> 1*
               l10(9) -> 10*
               l10(1) -> 1*
               l20(42) -> 43*
               l20(2) -> 2*
               l20(1) -> 2*
               b0(2) -> 6*
               b0(26) -> 27*
               b0(1) -> 6*
               b0(28) -> 29*
               1 -> 38,8
               2 -> 38,8
               3 -> 26*
               4 -> 7*
               5 -> 28*
               7 -> 112,9
               8 -> 38,42
               9 -> 37*
               10 -> 78,112,4
               27 -> 6*
               29 -> 6*
               37 -> 78,39
               38 -> 40*
               39 -> 78*
               40 -> 77*
               41 -> 38,8
               42 -> 111*
               43 -> 38,8
               77 -> 8,38
               78 -> 7*
               111 -> 38*
               112 -> 7*
             problem:
              strict:
               a(l1(x1)) -> l1(a(a(a(x1))))
               a(a(l2(x1))) -> l2(a(a(x1)))
              weak:
               r2(a(x1)) -> a(a(a(r2(x1))))
               r1(a(x1)) -> a(a(a(r1(x1))))
               r1(b(x1)) -> l1(b(x1))
               r2(b(x1)) -> l2(a(b(x1)))
               a(a(x1)) -> x1
               b(l1(x1)) -> b(r2(x1))
               b(l2(x1)) -> b(r1(x1))
             Open