MAYBE

Problem:
 a(l(x1)) -> l(a(x1))
 r(a(a(x1))) -> a(a(r(x1)))
 b(l(x1)) -> b(a(r(x1)))
 r(b(x1)) -> l(b(x1))

Proof:
 Complexity Transformation Processor:
  strict:
   a(l(x1)) -> l(a(x1))
   r(a(a(x1))) -> a(a(r(x1)))
   b(l(x1)) -> b(a(r(x1)))
   r(b(x1)) -> l(b(x1))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [b](x0) = x0,
     
     [r](x0) = x0 + 1,
     
     [a](x0) = x0,
     
     [l](x0) = x0
    orientation:
     a(l(x1)) = x1 >= x1 = l(a(x1))
     
     r(a(a(x1))) = x1 + 1 >= x1 + 1 = a(a(r(x1)))
     
     b(l(x1)) = x1 >= x1 + 1 = b(a(r(x1)))
     
     r(b(x1)) = x1 + 1 >= x1 = l(b(x1))
    problem:
     strict:
      a(l(x1)) -> l(a(x1))
      r(a(a(x1))) -> a(a(r(x1)))
      b(l(x1)) -> b(a(r(x1)))
     weak:
      r(b(x1)) -> l(b(x1))
    Bounds Processor:
     bound: 3
     enrichment: match
     automaton:
      final states: {5}
      transitions:
       b3(234) -> 235*
       a3(526) -> 527*
       a3(506) -> 507*
       a3(578) -> 579*
       a3(468) -> 469*
       a3(525) -> 526*
       a3(233) -> 234*
       a3(380) -> 381*
       a3(577) -> 578*
       a3(507) -> 508*
       a3(509) -> 510*
       l1(51) -> 52*
       r3(232) -> 233*
       r3(576) -> 577*
       r3(383) -> 384*
       r3(505) -> 506*
       r3(524) -> 525*
       a1(267) -> 268*
       a1(25) -> 26*
       a1(266) -> 267*
       a1(116) -> 117*
       a1(28) -> 29*
       b2(329) -> 330*
       b2(186) -> 187*
       b2(96) -> 97*
       b2(165) -> 166*
       r1(24) -> 25*
       r1(265) -> 266*
       r1(53) -> 54*
       b1(72) -> 73*
       b1(26) -> 27*
       a2(449) -> 450*
       a2(207) -> 208*
       a2(486) -> 487*
       a2(401) -> 402*
       a2(548) -> 549*
       a2(286) -> 287*
       a2(288) -> 289*
       a2(485) -> 486*
       a2(547) -> 548*
       a2(285) -> 286*
       a2(417) -> 418*
       a2(95) -> 96*
       a0(5) -> 5*
       r2(546) -> 547*
       r2(284) -> 285*
       r2(94) -> 95*
       r2(230) -> 231*
       r2(484) -> 485*
       l0(5) -> 5*
       l2(289) -> 290*
       l2(208) -> 209*
       l2(330) -> 331*
       l2(402) -> 403*
       l2(135) -> 136*
       r0(5) -> 5*
       l3(469) -> 470*
       l3(381) -> 382*
       l3(327) -> 328*
       b0(5) -> 5*
       5 -> 72,24
       26 -> 186,28
       27 -> 166,73,51,5
       29 -> 25*
       51 -> 116,94,53
       52 -> 268,267,266,29,54,26,25,5
       54 -> 25*
       72 -> 165*
       73 -> 51*
       97 -> 187,166,135,27,73
       116 -> 284,265
       117 -> 51*
       135 -> 207*
       136 -> 285,266,95,54
       166 -> 135*
       187 -> 135*
       208 -> 288,232,230
       209 -> 286,267,96,26
       231 -> 95*
       234 -> 329*
       235 -> 327,97,187
       268 -> 266,54
       287 -> 285,95
       288 -> 505,484
       289 -> 417*
       290 -> 287,268,29
       327 -> 380*
       328 -> 285,95
       330 -> 401*
       331 -> 266*
       381 -> 468,383
       382 -> 286,96
       384 -> 233*
       402 -> 449*
       403 -> 267*
       418 -> 208*
       449 -> 546,524
       450 -> 289*
       468 -> 576*
       469 -> 509*
       470 -> 287*
       487 -> 485,231
       508 -> 506,233
       510 -> 381*
       527 -> 233,506
       549 -> 231,485
       579 -> 577,384
     problem:
      strict:
       a(l(x1)) -> l(a(x1))
       r(a(a(x1))) -> a(a(r(x1)))
      weak:
       b(l(x1)) -> b(a(r(x1)))
       r(b(x1)) -> l(b(x1))
     Open