MAYBE
Time: 0.028404
TRS:
 {    f(x, f(y, z)) -> f(f(x, y), z),
  f(f(a(), b()), x) -> f(a(), f(a(), x)),
  f(f(b(), a()), x) -> f(b(), f(b(), x))}
 DP:
  DP:
   {    f#(x, f(y, z)) -> f#(x, y),
        f#(x, f(y, z)) -> f#(f(x, y), z),
    f#(f(a(), b()), x) -> f#(a(), x),
    f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
    f#(f(b(), a()), x) -> f#(b(), x),
    f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
  TRS:
  {    f(x, f(y, z)) -> f(f(x, y), z),
   f(f(a(), b()), x) -> f(a(), f(a(), x)),
   f(f(b(), a()), x) -> f(b(), f(b(), x))}
  UR:
   {    f(x, f(y, z)) -> f(f(x, y), z),
    f(f(a(), b()), x) -> f(a(), f(a(), x)),
    f(f(b(), a()), x) -> f(b(), f(b(), x))}
   EDG:
    {(f#(f(b(), a()), x) -> f#(b(), f(b(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))
     (f#(f(b(), a()), x) -> f#(b(), f(b(), x)), f#(x, f(y, z)) -> f#(x, y))
     (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), f(b(), x)))
     (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), x))
     (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(a(), f(a(), x)))
     (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), 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(b(), a()), x) -> f#(b(), x), f#(x, f(y, z)) -> f#(f(x, y), z))
     (f#(f(b(), a()), x) -> f#(b(), x), f#(x, f(y, z)) -> f#(x, y))
     (f#(f(a(), b()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(x, y))
     (f#(f(a(), b()), 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(), b()), x) -> f#(a(), x))
     (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), b()), x) -> f#(a(), f(a(), x)))
     (f#(x, f(y, z)) -> f#(x, y), f#(f(b(), a()), x) -> f#(b(), x))
     (f#(x, f(y, z)) -> f#(x, y), f#(f(b(), a()), x) -> f#(b(), f(b(), x)))
     (f#(f(a(), b()), x) -> f#(a(), f(a(), x)), f#(x, f(y, z)) -> f#(x, y))
     (f#(f(a(), b()), x) -> f#(a(), f(a(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))}
    STATUS:
     arrows: 0.444444
     SCCS (1):
      Scc:
       {    f#(x, f(y, z)) -> f#(x, y),
            f#(x, f(y, z)) -> f#(f(x, y), z),
        f#(f(a(), b()), x) -> f#(a(), x),
        f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
        f#(f(b(), a()), x) -> f#(b(), x),
        f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
      
      SCC (6):
       Strict:
        {    f#(x, f(y, z)) -> f#(x, y),
             f#(x, f(y, z)) -> f#(f(x, y), z),
         f#(f(a(), b()), x) -> f#(a(), x),
         f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
         f#(f(b(), a()), x) -> f#(b(), x),
         f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
       Weak:
       {    f(x, f(y, z)) -> f(f(x, y), z),
        f(f(a(), b()), x) -> f(a(), f(a(), x)),
        f(f(b(), a()), x) -> f(b(), f(b(), x))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0, x1) = x0 + x1,
         
         [a] = 1,
         
         [b] = 1,
         
         [f#](x0, x1) = x0 + x1
        Strict:
         f#(f(b(), a()), x) -> f#(b(), f(b(), x))
         2 + 1x >= 2 + 1x
         f#(f(b(), a()), x) -> f#(b(), x)
         2 + 1x >= 1 + 1x
         f#(f(a(), b()), x) -> f#(a(), f(a(), x))
         2 + 1x >= 2 + 1x
         f#(f(a(), b()), x) -> f#(a(), x)
         2 + 1x >= 1 + 1x
         f#(x, f(y, z)) -> f#(f(x, y), z)
         0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
         f#(x, f(y, z)) -> f#(x, y)
         0 + 1x + 1y + 1z >= 0 + 1x + 1y
        Weak:
         f(f(b(), a()), x) -> f(b(), f(b(), x))
         2 + 1x >= 2 + 1x
         f(f(a(), b()), x) -> f(a(), f(a(), x))
         2 + 1x >= 2 + 1x
         f(x, f(y, z)) -> f(f(x, y), z)
         0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z
       SCCS (1):
        Scc:
         {    f#(x, f(y, z)) -> f#(x, y),
              f#(x, f(y, z)) -> f#(f(x, y), z),
          f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
          f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
        
        SCC (4):
         Strict:
          {    f#(x, f(y, z)) -> f#(x, y),
               f#(x, f(y, z)) -> f#(f(x, y), z),
           f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
           f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
         Weak:
         {    f(x, f(y, z)) -> f(f(x, y), z),
          f(f(a(), b()), x) -> f(a(), f(a(), x)),
          f(f(b(), a()), x) -> f(b(), f(b(), x))}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [f](x0, x1) = x0 + x1 + 1,
           
           [a] = 1,
           
           [b] = 1,
           
           [f#](x0, x1) = x0 + x1
          Strict:
           f#(f(b(), a()), x) -> f#(b(), f(b(), x))
           3 + 1x >= 3 + 1x
           f#(f(a(), b()), x) -> f#(a(), f(a(), x))
           3 + 1x >= 3 + 1x
           f#(x, f(y, z)) -> f#(f(x, y), z)
           1 + 1x + 1y + 1z >= 1 + 1x + 1y + 1z
           f#(x, f(y, z)) -> f#(x, y)
           1 + 1x + 1y + 1z >= 0 + 1x + 1y
          Weak:
           f(f(b(), a()), x) -> f(b(), f(b(), x))
           4 + 1x >= 4 + 1x
           f(f(a(), b()), x) -> f(a(), f(a(), x))
           4 + 1x >= 4 + 1x
           f(x, f(y, z)) -> f(f(x, y), z)
           2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z
         SCCS (1):
          Scc:
           {    f#(x, f(y, z)) -> f#(f(x, y), z),
            f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
            f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
          
          SCC (3):
           Strict:
            {    f#(x, f(y, z)) -> f#(f(x, y), z),
             f#(f(a(), b()), x) -> f#(a(), f(a(), x)),
             f#(f(b(), a()), x) -> f#(b(), f(b(), x))}
           Weak:
           {    f(x, f(y, z)) -> f(f(x, y), z),
            f(f(a(), b()), x) -> f(a(), f(a(), x)),
            f(f(b(), a()), x) -> f(b(), f(b(), x))}
           Fail