MAYBE
Time: 0.001640
TRS:
 {f(x, a b y) -> f(a a x, y),
  f(x, b a y) -> f(b b x, y),
    f(a x, y) -> f(x, a y),
    f(b x, y) -> f(x, b y)}
 DP:
  DP:
   {f#(x, a b y) -> f#(a a x, y),
    f#(x, b a y) -> f#(b b x, y),
      f#(a x, y) -> f#(x, a y),
      f#(b x, y) -> f#(x, b y)}
  TRS:
  {f(x, a b y) -> f(a a x, y),
   f(x, b a y) -> f(b b x, y),
     f(a x, y) -> f(x, a y),
     f(b x, y) -> f(x, b y)}
  EDG:
   {(f#(x, b a y) -> f#(b b x, y), f#(b x, y) -> f#(x, b y))
    (f#(x, b a y) -> f#(b b x, y), f#(x, b a y) -> f#(b b x, y))
    (f#(x, b a y) -> f#(b b x, y), f#(x, a b y) -> f#(a a x, y))
    (f#(b x, y) -> f#(x, b y), f#(b x, y) -> f#(x, b y))
    (f#(b x, y) -> f#(x, b y), f#(a x, y) -> f#(x, a y))
    (f#(b x, y) -> f#(x, b y), f#(x, b a y) -> f#(b b x, y))
    (f#(a x, y) -> f#(x, a y), f#(x, a b y) -> f#(a a x, y))
    (f#(a x, y) -> f#(x, a y), f#(a x, y) -> f#(x, a y))
    (f#(a x, y) -> f#(x, a y), f#(b x, y) -> f#(x, b y))
    (f#(x, a b y) -> f#(a a x, y), f#(x, a b y) -> f#(a a x, y))
    (f#(x, a b y) -> f#(a a x, y), f#(x, b a y) -> f#(b b x, y))
    (f#(x, a b y) -> f#(a a x, y), f#(a x, y) -> f#(x, a y))}
   STATUS:
    arrows: 0.250000
    SCCS (1):
     Scc:
      {f#(x, a b y) -> f#(a a x, y),
       f#(x, b a y) -> f#(b b x, y),
         f#(a x, y) -> f#(x, a y),
         f#(b x, y) -> f#(x, b y)}
     
     SCC (4):
      Strict:
       {f#(x, a b y) -> f#(a a x, y),
        f#(x, b a y) -> f#(b b x, y),
          f#(a x, y) -> f#(x, a y),
          f#(b x, y) -> f#(x, b y)}
      Weak:
      {f(x, a b y) -> f(a a x, y),
       f(x, b a y) -> f(b b x, y),
         f(a x, y) -> f(x, a y),
         f(b x, y) -> f(x, b y)}
      Open