MAYBE
Time: 0.036797
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)}
      Open