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