MAYBE
Time: 0.005687
TRS:
 {    f(x, f(y, z)) -> f(f(x, y), z),
  f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
 DP:
  DP:
   {    f#(x, f(y, z)) -> f#(x, y),
        f#(x, f(y, z)) -> f#(f(x, y), z),
    f#(f(a(), a()), x) -> f#(a(), x),
    f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))),
    f#(f(a(), a()), x) -> f#(b(), f(a(), x))}
  TRS:
  {    f(x, f(y, z)) -> f(f(x, y), z),
   f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
  UR:
   {    f(x, f(y, z)) -> f(f(x, y), z),
    f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
   EDG:
    {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))
     (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
     (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), x))
     (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))
     (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y))
     (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))
     (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
     (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(f(a(), a()), x) -> f#(a(), x))
     (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))
     (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(x, y))
     (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(x, y))
     (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(f(x, y), z))
     (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(f(a(), a()), x) -> f#(a(), x))
     (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
     (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))
     (f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(x, y))
     (f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(f(x, y), z))
     (f#(f(a(), a()), x) -> f#(a(), x), f#(f(a(), a()), x) -> f#(a(), x))
     (f#(f(a(), a()), x) -> f#(a(), x), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
     (f#(f(a(), a()), x) -> f#(a(), x), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))
     (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y))
     (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z))
     (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), x))
     (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
     (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))}
    EDG:
     {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))
      (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
      (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), x))
      (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))
      (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y))
      (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))
      (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(x, y))
      (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(x, y))
      (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(f(x, y), z))
      (f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(x, y))
      (f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(f(x, y), z))
      (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y))
      (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z))
      (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), x))
      (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
      (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))}
     EDG:
      {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))
       (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
       (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), x))
       (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))
       (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y))
       (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))
       (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(x, y))
       (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(x, y))
       (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(f(x, y), z))
       (f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(x, y))
       (f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(f(x, y), z))
       (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y))
       (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z))
       (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), x))
       (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
       (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))}
      EDG:
       {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))
        (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
        (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), a()), x) -> f#(a(), x))
        (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))
        (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y))
        (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))
        (f#(f(a(), a()), x) -> f#(b(), f(a(), x)), f#(x, f(y, z)) -> f#(x, y))
        (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(x, y))
        (f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))), f#(x, f(y, z)) -> f#(f(x, y), z))
        (f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(x, y))
        (f#(f(a(), a()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(f(x, y), z))
        (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y))
        (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z))
        (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), x))
        (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))))
        (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), a()), x) -> f#(b(), f(a(), x)))}
       STATUS:
        arrows: 0.360000
        SCCS (1):
         Scc:
          {    f#(x, f(y, z)) -> f#(x, y),
               f#(x, f(y, z)) -> f#(f(x, y), z),
           f#(f(a(), a()), x) -> f#(a(), x),
           f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))),
           f#(f(a(), a()), x) -> f#(b(), f(a(), x))}
         
         SCC (5):
          Strict:
           {    f#(x, f(y, z)) -> f#(x, y),
                f#(x, f(y, z)) -> f#(f(x, y), z),
            f#(f(a(), a()), x) -> f#(a(), x),
            f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x))),
            f#(f(a(), a()), x) -> f#(b(), f(a(), x))}
          Weak:
          {    f(x, f(y, z)) -> f(f(x, y), z),
           f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
          Open