MAYBE
Time: 0.006927
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))}
  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, 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)))}
   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))}
     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 (1):
        Scc:
         {*#(*(x, y), z) -> *#(x, *(y, z)),
          *#(*(x, y), z) -> *#(y, z),
          *#(+(x, y), z) -> *#(y, z)}
        SCC (3):
         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 (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))}
             SPSC:
              Simple Projection:
               pi(*#) = 0
              Strict:
               {*#(+(x, y), z) -> *#(y, z)}
              EDG:
               {(*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z))}
               SCCS (1):
                Scc:
                 {*#(+(x, y), z) -> *#(y, z)}
                SCC (1):
                 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 (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