MAYBE
Time: 0.016882
TRS:
 {  f(x, y, g z) -> g f(x, y, z),
    f(x, g y, z) -> g f(x, y, z),
    f(g x, y, z) -> g f(x, y, z),
  f(0(), 1(), x) -> f(g x, g x, x)}
 DP:
  DP:
   {  f#(x, y, g z) -> f#(x, y, z),
      f#(x, g y, z) -> f#(x, y, z),
      f#(g x, y, z) -> f#(x, y, z),
    f#(0(), 1(), x) -> f#(g x, g x, x)}
  TRS:
  {  f(x, y, g z) -> g f(x, y, z),
     f(x, g y, z) -> g f(x, y, z),
     f(g x, y, z) -> g f(x, y, z),
   f(0(), 1(), x) -> f(g x, g x, x)}
  UR:
   {a(w, v) -> w,
    a(w, v) -> v}
   EDG:
    {(f#(x, y, g z) -> f#(x, y, z), f#(0(), 1(), x) -> f#(g x, g x, x))
     (f#(x, y, g z) -> f#(x, y, z), f#(g x, y, z) -> f#(x, y, z))
     (f#(x, y, g z) -> f#(x, y, z), f#(x, g y, z) -> f#(x, y, z))
     (f#(x, y, g z) -> f#(x, y, z), f#(x, y, g z) -> f#(x, y, z))
     (f#(g x, y, z) -> f#(x, y, z), f#(0(), 1(), x) -> f#(g x, g x, x))
     (f#(g x, y, z) -> f#(x, y, z), f#(g x, y, z) -> f#(x, y, z))
     (f#(g x, y, z) -> f#(x, y, z), f#(x, g y, z) -> f#(x, y, z))
     (f#(g x, y, z) -> f#(x, y, z), f#(x, y, g z) -> f#(x, y, z))
     (f#(x, g y, z) -> f#(x, y, z), f#(x, y, g z) -> f#(x, y, z))
     (f#(x, g y, z) -> f#(x, y, z), f#(x, g y, z) -> f#(x, y, z))
     (f#(x, g y, z) -> f#(x, y, z), f#(g x, y, z) -> f#(x, y, z))
     (f#(x, g y, z) -> f#(x, y, z), f#(0(), 1(), x) -> f#(g x, g x, x))
     (f#(0(), 1(), x) -> f#(g x, g x, x), f#(x, y, g z) -> f#(x, y, z))
     (f#(0(), 1(), x) -> f#(g x, g x, x), f#(x, g y, z) -> f#(x, y, z))
     (f#(0(), 1(), x) -> f#(g x, g x, x), f#(g x, y, z) -> f#(x, y, z))}
    STATUS:
     arrows: 0.062500
     SCCS (1):
      Scc:
       {  f#(x, y, g z) -> f#(x, y, z),
          f#(x, g y, z) -> f#(x, y, z),
          f#(g x, y, z) -> f#(x, y, z),
        f#(0(), 1(), x) -> f#(g x, g x, x)}
      
      SCC (4):
       Strict:
        {  f#(x, y, g z) -> f#(x, y, z),
           f#(x, g y, z) -> f#(x, y, z),
           f#(g x, y, z) -> f#(x, y, z),
         f#(0(), 1(), x) -> f#(g x, g x, x)}
       Weak:
       {  f(x, y, g z) -> g f(x, y, z),
          f(x, g y, z) -> g f(x, y, z),
          f(g x, y, z) -> g f(x, y, z),
        f(0(), 1(), x) -> f(g x, g x, x)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [f](x0, x1, x2) = x0 + 1,
         
         [g](x0) = x0 + 1,
         
         [0] = 0,
         
         [1] = 0,
         
         [f#](x0, x1, x2) = x0
        Strict:
         f#(0(), 1(), x) -> f#(g x, g x, x)
         0 + 1x >= 0 + 1x
         f#(g x, y, z) -> f#(x, y, z)
         0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z
         f#(x, g y, z) -> f#(x, y, z)
         0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z
         f#(x, y, g z) -> f#(x, y, z)
         1 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z
        Weak:
         f(0(), 1(), x) -> f(g x, g x, x)
         1 + 1x >= 1 + 1x
         f(g x, y, z) -> g f(x, y, z)
         1 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z
         f(x, g y, z) -> g f(x, y, z)
         1 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z
         f(x, y, g z) -> g f(x, y, z)
         2 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z
       SCCS (1):
        Scc:
         {  f#(x, g y, z) -> f#(x, y, z),
            f#(g x, y, z) -> f#(x, y, z),
          f#(0(), 1(), x) -> f#(g x, g x, x)}
        
        SCC (3):
         Strict:
          {  f#(x, g y, z) -> f#(x, y, z),
             f#(g x, y, z) -> f#(x, y, z),
           f#(0(), 1(), x) -> f#(g x, g x, x)}
         Weak:
         {  f(x, y, g z) -> g f(x, y, z),
            f(x, g y, z) -> g f(x, y, z),
            f(g x, y, z) -> g f(x, y, z),
          f(0(), 1(), x) -> f(g x, g x, x)}
         Fail