MAYBE
TRS:
 {f(f(f(a(), f(a(), a())), a()), x) -> f(x, f(x, a()))}
 DP:
  Strict:
   {f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, f(x, a())),
    f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, a())}
  Weak:
  {f(f(f(a(), f(a(), a())), a()), x) -> f(x, f(x, a()))}
  EDG:
   {(f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, a()), f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, a()))
    (f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, a()), f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, f(x, a())))
    (f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, f(x, a())), f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, f(x, a())))
    (f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, f(x, a())), f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, a()))}
   SCCS:
    Scc:
     {f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, f(x, a())),
      f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, a())}
    SCC:
     Strict:
      {f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, f(x, a())),
       f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, a())}
     Weak:
     {f(f(f(a(), f(a(), a())), a()), x) -> f(x, f(x, a()))}
     POLY:
      Argument Filtering:
       pi(a) = [], pi(f#) = [0,1], pi(f) = []
      Usable Rules:
       {}
      Interpretation:
       [f#](x0, x1) = x0 + x1,
       [f] = 1,
       [a] = 0
      Strict:
       {f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, f(x, a()))}
      Weak:
       {f(f(f(a(), f(a(), a())), a()), x) -> f(x, f(x, a()))}
      EDG:
       {(f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, f(x, a())), f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, f(x, a())))}
       SCCS:
        Scc:
         {f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, f(x, a()))}
        SCC:
         Strict:
          {f#(f(f(a(), f(a(), a())), a()), x) -> f#(x, f(x, a()))}
         Weak:
         {f(f(f(a(), f(a(), a())), a()), x) -> f(x, f(x, a()))}
         Fail