MAYBE
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:
  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),
    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)))))}
  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))))))}
  EDG:
   {(a#(a(f(x, y))) -> a#(y), a#(a(f(x, y))) -> a#(b(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(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#(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))) -> 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#(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#(a(x), a(y)) -> f#(x, y))
    (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)) -> 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(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#(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))) -> f#(a(b(a(b(a(x))))), a(b(a(b(a(y)))))))
    (f#(b(x), b(y)) -> f#(x, y), f#(a(x), a(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#(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)))))), f#(a(x), a(y)) -> 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), 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#(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#(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(b(a(x))))))
    (a#(a(f(x, y))) -> a#(x), a#(a(f(x, y))) -> a#(b(a(b(a(y))))))}
   SCCS:
    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:
     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:
      Argument Filtering:
       pi(b) = 0, pi(a#) = 0, pi(a) = 0, pi(f#) = [0,1], pi(f) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [f#](x0, x1) = x0 + x1 + 1,
       [f](x0, x1) = x0 + x1 + 1
      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))))))}
      EDG:
       {(f#(a(x), a(y)) -> f#(x, y), f#(b(x), b(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#(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))
        (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)))))))
        (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))
        (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)))}
       SCCS:
        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:
         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