MAYBE

Problem:
 *(*(x,y),z) -> *(x,*(y,z))
 *(+(x,y),z) -> +(*(x,z),*(y,z))
 *(x,+(y,f(z))) -> *(g(x,z),+(y,y))

Proof:
 DP Processor:
  DPs:
   *#(*(x,y),z) -> *#(y,z)
   *#(*(x,y),z) -> *#(x,*(y,z))
   *#(+(x,y),z) -> *#(y,z)
   *#(+(x,y),z) -> *#(x,z)
   *#(x,+(y,f(z))) -> *#(g(x,z),+(y,y))
  TRS:
   *(*(x,y),z) -> *(x,*(y,z))
   *(+(x,y),z) -> +(*(x,z),*(y,z))
   *(x,+(y,f(z))) -> *(g(x,z),+(y,y))
  EDG Processor:
   DPs:
    *#(*(x,y),z) -> *#(y,z)
    *#(*(x,y),z) -> *#(x,*(y,z))
    *#(+(x,y),z) -> *#(y,z)
    *#(+(x,y),z) -> *#(x,z)
    *#(x,+(y,f(z))) -> *#(g(x,z),+(y,y))
   TRS:
    *(*(x,y),z) -> *(x,*(y,z))
    *(+(x,y),z) -> +(*(x,z),*(y,z))
    *(x,+(y,f(z))) -> *(g(x,z),+(y,y))
   graph:
    *#(+(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) -> *#(y,z)
    *#(+(x,y),z) -> *#(y,z) -> *#(+(x,y),z) -> *#(x,z)
    *#(+(x,y),z) -> *#(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,*(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,f(z))) -> *#(g(x,z),+(y,y))
    *#(*(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) -> *#(y,z)
    *#(*(x,y),z) -> *#(y,z) -> *#(+(x,y),z) -> *#(x,z)
    *#(*(x,y),z) -> *#(y,z) -> *#(x,+(y,f(z))) -> *#(g(x,z),+(y,y))
    *#(*(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),z) -> *#(y,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))
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 20/25
    DPs:
     *#(+(x,y),z) -> *#(y,z)
     *#(+(x,y),z) -> *#(x,z)
     *#(*(x,y),z) -> *#(x,*(y,z))
     *#(*(x,y),z) -> *#(y,z)
    TRS:
     *(*(x,y),z) -> *(x,*(y,z))
     *(+(x,y),z) -> +(*(x,z),*(y,z))
     *(x,+(y,f(z))) -> *(g(x,z),+(y,y))
    Subterm Criterion Processor:
     simple projection:
      pi(*#) = 0
     problem:
      DPs:
       
      TRS:
       *(*(x,y),z) -> *(x,*(y,z))
       *(+(x,y),z) -> +(*(x,z),*(y,z))
       *(x,+(y,f(z))) -> *(g(x,z),+(y,y))
     Qed
    
    DPs:
     *#(x,+(y,f(z))) -> *#(g(x,z),+(y,y))
    TRS:
     *(*(x,y),z) -> *(x,*(y,z))
     *(+(x,y),z) -> +(*(x,z),*(y,z))
     *(x,+(y,f(z))) -> *(g(x,z),+(y,y))
    Open