MAYBE
Time: 0.010694
TRS:
 {            +(x, +(y, z)) -> +(+(x, y), z),
        +(*(x, y), +(x, z)) -> *(x, +(y, z)),
  +(*(x, y), +(*(x, z), u)) -> +(*(x, +(y, z)), u)}
 DP:
  DP:
   {            +#(x, +(y, z)) -> +#(x, y),
                +#(x, +(y, z)) -> +#(+(x, y), z),
          +#(*(x, y), +(x, z)) -> +#(y, z),
    +#(*(x, y), +(*(x, z), u)) -> +#(y, z),
    +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u)}
  TRS:
  {            +(x, +(y, z)) -> +(+(x, y), z),
         +(*(x, y), +(x, z)) -> *(x, +(y, z)),
   +(*(x, y), +(*(x, z), u)) -> +(*(x, +(y, z)), u)}
  EDG:
   {(+#(x, +(y, z)) -> +#(+(x, y), z), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(*(x, y), +(*(x, z), u)) -> +#(y, z))
    (+#(x, +(y, z)) -> +#(+(x, y), z), +#(*(x, y), +(x, 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))
    (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))
    (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(*(x, y), +(*(x, z), u)) -> +#(y, z))
    (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(*(x, y), +(x, z)) -> +#(y, z))
    (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(x, +(y, z)) -> +#(x, y))
    (+#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u), +#(x, +(y, z)) -> +#(x, y))
    (+#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u), +#(*(x, y), +(x, z)) -> +#(y, z))
    (+#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u), +#(*(x, y), +(*(x, z), u)) -> +#(y, z))
    (+#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))
    (+#(*(x, y), +(x, z)) -> +#(y, z), +#(x, +(y, z)) -> +#(x, y))
    (+#(*(x, y), +(x, z)) -> +#(y, z), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(*(x, y), +(x, z)) -> +#(y, z), +#(*(x, y), +(x, z)) -> +#(y, z))
    (+#(*(x, y), +(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u)) -> +#(y, z))
    (+#(*(x, y), +(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))
    (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
    (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
    (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(x, z)) -> +#(y, z))
    (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(*(x, z), u)) -> +#(y, z))
    (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))}
   EDG:
    {(+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))
     (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(*(x, y), +(*(x, z), u)) -> +#(y, z))
     (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(*(x, y), +(x, z)) -> +#(y, z))
     (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(x, +(y, z)) -> +#(+(x, y), z))
     (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(x, +(y, z)) -> +#(x, y))
     (+#(*(x, y), +(x, z)) -> +#(y, z), +#(x, +(y, z)) -> +#(x, y))
     (+#(*(x, y), +(x, z)) -> +#(y, z), +#(x, +(y, z)) -> +#(+(x, y), z))
     (+#(*(x, y), +(x, z)) -> +#(y, z), +#(*(x, y), +(x, z)) -> +#(y, z))
     (+#(*(x, y), +(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u)) -> +#(y, z))
     (+#(*(x, y), +(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
     (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(x, z)) -> +#(y, z))
     (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(*(x, z), u)) -> +#(y, z))
     (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))}
    EDG:
     {(+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))
      (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(*(x, y), +(*(x, z), u)) -> +#(y, z))
      (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(*(x, y), +(x, z)) -> +#(y, z))
      (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(x, +(y, z)) -> +#(+(x, y), z))
      (+#(*(x, y), +(*(x, z), u)) -> +#(y, z), +#(x, +(y, z)) -> +#(x, y))
      (+#(*(x, y), +(x, z)) -> +#(y, z), +#(x, +(y, z)) -> +#(x, y))
      (+#(*(x, y), +(x, z)) -> +#(y, z), +#(x, +(y, z)) -> +#(+(x, y), z))
      (+#(*(x, y), +(x, z)) -> +#(y, z), +#(*(x, y), +(x, z)) -> +#(y, z))
      (+#(*(x, y), +(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u)) -> +#(y, z))
      (+#(*(x, y), +(x, z)) -> +#(y, z), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))
      (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
      (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
      (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(x, z)) -> +#(y, z))
      (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(*(x, z), u)) -> +#(y, z))
      (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))}
     STATUS:
      arrows: 0.400000
      SCCS (1):
       Scc:
        {            +#(x, +(y, z)) -> +#(x, y),
               +#(*(x, y), +(x, z)) -> +#(y, z),
         +#(*(x, y), +(*(x, z), u)) -> +#(y, z)}
       
       SCC (3):
        Strict:
         {            +#(x, +(y, z)) -> +#(x, y),
                +#(*(x, y), +(x, z)) -> +#(y, z),
          +#(*(x, y), +(*(x, z), u)) -> +#(y, z)}
        Weak:
        {            +(x, +(y, z)) -> +(+(x, y), z),
               +(*(x, y), +(x, z)) -> *(x, +(y, z)),
         +(*(x, y), +(*(x, z), u)) -> +(*(x, +(y, z)), u)}
        Open