YES
Time: 0.028267
TRS:
 {b b a x -> a b b x,
    a a x -> b b x}
 DP:
  DP:
   {b# b a x -> b# x,
    b# b a x -> b# b x,
    b# b a x -> a# b b x,
      a# a x -> b# x,
      a# a x -> b# b x}
  TRS:
  {b b a x -> a b b x,
     a a x -> b b x}
  UR:
   {b b a x -> a b b x,
      a a x -> b b x}
   EDG:
    {(b# b a x -> a# b b x, a# a x -> b# b x)
     (b# b a x -> a# b b x, a# a x -> b# x)
     (b# b a x -> b# x, b# b a x -> a# b b x)
     (b# b a x -> b# x, b# b a x -> b# b x)
     (b# b a x -> b# x, b# b a x -> b# x)
     (a# a x -> b# x, b# b a x -> b# x)
     (a# a x -> b# x, b# b a x -> b# b x)
     (a# a x -> b# x, b# b a x -> a# b b x)
     (a# a x -> b# b x, b# b a x -> b# x)
     (a# a x -> b# b x, b# b a x -> b# b x)
     (a# a x -> b# b x, b# b a x -> a# b b x)
     (b# b a x -> b# b x, b# b a x -> b# x)
     (b# b a x -> b# b x, b# b a x -> b# b x)
     (b# b a x -> b# b x, b# b a x -> a# b b x)}
    STATUS:
     arrows: 0.440000
     SCCS (1):
      Scc:
       {b# b a x -> b# x,
        b# b a x -> b# b x,
        b# b a x -> a# b b x,
          a# a x -> b# x,
          a# a x -> b# b x}
      
      SCC (5):
       Strict:
        {b# b a x -> b# x,
         b# b a x -> b# b x,
         b# b a x -> a# b b x,
           a# a x -> b# x,
           a# a x -> b# b x}
       Weak:
       {b b a x -> a b b x,
          a a x -> b b x}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [b](x0) = x0,
         
         [a](x0) = x0 + 1,
         
         [b#](x0) = x0,
         
         [a#](x0) = x0
        Strict:
         a# a x -> b# b x
         1 + 1x >= 0 + 1x
         a# a x -> b# x
         1 + 1x >= 0 + 1x
         b# b a x -> a# b b x
         1 + 1x >= 0 + 1x
         b# b a x -> b# b x
         1 + 1x >= 0 + 1x
         b# b a x -> b# x
         1 + 1x >= 0 + 1x
        Weak:
         a a x -> b b x
         2 + 1x >= 0 + 1x
         b b a x -> a b b x
         1 + 1x >= 1 + 1x
       Qed