YES
Time: 0.004984
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}
  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)}
   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:
       
     Qed