MAYBE
TRS:
 {*(x, +(y, f(z))) -> *(g(x, z), +(y, y)),
     *(*(x, y), z) -> *(x, *(y, z)),
     *(+(x, y), z) -> +(*(x, z), *(y, z))}
 DP:
  Strict:
   {*#(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)}
  Weak:
  {*(x, +(y, f(z))) -> *(g(x, z), +(y, y)),
      *(*(x, y), z) -> *(x, *(y, z)),
      *(+(x, y), z) -> +(*(x, z), *(y, z))}
  EDG:
   {(*#(+(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, f(z))) -> *#(g(x, z), +(y, y)), *#(x, +(y, f(z))) -> *#(g(x, z), +(y, y)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(*(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) -> *#(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))}
   SCCS:
    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:
     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))}
     SPSC:
      Simple Projection:
       pi(*#) = 0
      Strict:
       {*#(*(x, y), z) -> *#(x, *(y, z)),
        *#(*(x, y), z) -> *#(y, z),
        *#(+(x, y), z) -> *#(y, z)}
      EDG:
       {(*#(*(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z))
        (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))
        (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z)))
        (*#(+(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) -> *#(y, z))
        (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z)))
        (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z))
        (*#(*(x, y), z) -> *#(x, *(y, z)), *#(+(x, y), z) -> *#(y, z))}
       SCCS:
        Scc:
         {*#(*(x, y), z) -> *#(x, *(y, z)),
          *#(*(x, y), z) -> *#(y, z),
          *#(+(x, y), z) -> *#(y, z)}
        SCC:
         Strict:
          {*#(*(x, y), z) -> *#(x, *(y, z)),
           *#(*(x, y), z) -> *#(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))}
         SPSC:
          Simple Projection:
           pi(*#) = 0
          Strict:
           {*#(*(x, y), z) -> *#(x, *(y, z)),
            *#(+(x, y), z) -> *#(y, z)}
          EDG:
           {(*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(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), z) -> *#(x, *(y, z)), *#(+(x, y), z) -> *#(y, z))}
           SCCS:
            Scc:
             {*#(*(x, y), z) -> *#(x, *(y, z)),
              *#(+(x, y), z) -> *#(y, z)}
            SCC:
             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))}
             SPSC:
              Simple Projection:
               pi(*#) = 0
              Strict:
               {*#(+(x, y), z) -> *#(y, z)}
              EDG:
               {(*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z))}
               SCCS:
                Scc:
                 {*#(+(x, y), z) -> *#(y, z)}
                SCC:
                 Strict:
                  {*#(+(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))}
                 SPSC:
                  Simple Projection:
                   pi(*#) = 0
                  Strict:
                   {}
                  Qed
    SCC:
     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