MAYBE
Time: 0.017060
TRS:
 {    f(a x, b()) -> f(b(), a x),
            a a x -> f(b(), a f(a x, b())),
  a a f(b(), a x) -> f(a a a x, b())}
 DP:
  DP:
   {    f#(a x, b()) -> f#(b(), a x),
              a# a x -> f#(a x, b()),
              a# a x -> f#(b(), a f(a x, b())),
              a# a x -> a# f(a x, b()),
    a# a f(b(), a x) -> f#(a a a x, b()),
    a# a f(b(), a x) -> a# a x,
    a# a f(b(), a x) -> a# a a x}
  TRS:
  {    f(a x, b()) -> f(b(), a x),
             a a x -> f(b(), a f(a x, b())),
   a a f(b(), a x) -> f(a a a x, b())}
  EDG:
   {(a# a x -> f#(a x, b()), f#(a x, b()) -> f#(b(), a x))
    (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> a# a a x)
    (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> a# a x)
    (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> f#(a a a x, b()))
    (a# a f(b(), a x) -> a# a x, a# a x -> a# f(a x, b()))
    (a# a f(b(), a x) -> a# a x, a# a x -> f#(b(), a f(a x, b())))
    (a# a f(b(), a x) -> a# a x, a# a x -> f#(a x, b()))
    (a# a f(b(), a x) -> f#(a a a x, b()), f#(a x, b()) -> f#(b(), a x))
    (a# a f(b(), a x) -> a# a a x, a# a x -> f#(a x, b()))
    (a# a f(b(), a x) -> a# a a x, a# a x -> f#(b(), a f(a x, b())))
    (a# a f(b(), a x) -> a# a a x, a# a x -> a# f(a x, b()))
    (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> f#(a a a x, b()))
    (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> a# a x)
    (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> a# a a x)}
   SCCS (1):
    Scc:
     {a# a f(b(), a x) -> a# a x,
      a# a f(b(), a x) -> a# a a x}
    SCC (2):
     Strict:
      {a# a f(b(), a x) -> a# a x,
       a# a f(b(), a x) -> a# a a x}
     Weak:
     {    f(a x, b()) -> f(b(), a x),
                a a x -> f(b(), a f(a x, b())),
      a a f(b(), a x) -> f(a a a x, b())}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [f](x0, x1) = x0 + x1,
       
       [a](x0) = x0 + 1,
       
       [b] = 0,
       
       [a#](x0) = x0
      Strict:
       a# a f(b(), a x) -> a# a a x
       2 + 1x >= 2 + 1x
       a# a f(b(), a x) -> a# a x
       2 + 1x >= 1 + 1x
      Weak:
       
     EDG:
      {(a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> a# a a x)}
      SCCS (1):
       Scc:
        {a# a f(b(), a x) -> a# a a x}
       SCC (1):
        Strict:
         {a# a f(b(), a x) -> a# a a x}
        Weak:
        {    f(a x, b()) -> f(b(), a x),
                   a a x -> f(b(), a f(a x, b())),
         a a f(b(), a x) -> f(a a a x, b())}
        Fail