MAYBE
Time: 0.057320
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#(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)))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0, x1) = x0,
         
         [a] = 1,
         
         [b] = 0,
         
         [f#](x0, x1) = x0
        Strict:
         f#(f(a(), a()), x) -> f#(b(), f(a(), x))
         1 + 0x >= 0 + 0x
         f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x)))
         1 + 0x >= 1 + 0x
         f#(f(a(), a()), x) -> f#(a(), x)
         1 + 0x >= 1 + 0x
         f#(x, f(y, z)) -> f#(f(x, y), z)
         0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z
         f#(x, f(y, z)) -> f#(x, y)
         0 + 1x + 0y + 0z >= 0 + 1x + 0y
        Weak:
         f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))
         1 + 0x >= 1 + 0x
         f(x, f(y, z)) -> f(f(x, y), z)
         0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z
       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)))}
        
        SCC (4):
         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)))}
         Weak:
         {    f(x, f(y, z)) -> f(f(x, y), z),
          f(f(a(), a()), x) -> f(a(), f(b(), f(a(), x)))}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [f](x0, x1) = x0 + x1,
           
           [a] = 1,
           
           [b] = 0,
           
           [f#](x0, x1) = x0 + x1
          Strict:
           f#(f(a(), a()), x) -> f#(a(), f(b(), f(a(), x)))
           2 + 1x >= 2 + 1x
           f#(f(a(), a()), 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(a(), a()), x) -> f(a(), f(b(), 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(), a()), x) -> f#(a(), f(b(), f(a(), x)))}
          
          SCC (3):
           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(), 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)))}
           Fail