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