MAYBE

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

Proof:
 DP Processor:
  DPs:
   +#(*(x,y),*(a(),y)) -> +#(x,a())
   +#(*(x,y),*(a(),y)) -> *#(+(x,a()),y)
   *#(*(x,y),z) -> *#(y,z)
   *#(*(x,y),z) -> *#(x,*(y,z))
  TRS:
   +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
   *(*(x,y),z) -> *(x,*(y,z))
  Usable Rule Processor:
   DPs:
    +#(*(x,y),*(a(),y)) -> +#(x,a())
    +#(*(x,y),*(a(),y)) -> *#(+(x,a()),y)
    *#(*(x,y),z) -> *#(y,z)
    *#(*(x,y),z) -> *#(x,*(y,z))
   TRS:
    *(*(x,y),z) -> *(x,*(y,z))
   EDG Processor:
    DPs:
     +#(*(x,y),*(a(),y)) -> +#(x,a())
     +#(*(x,y),*(a(),y)) -> *#(+(x,a()),y)
     *#(*(x,y),z) -> *#(y,z)
     *#(*(x,y),z) -> *#(x,*(y,z))
    TRS:
     *(*(x,y),z) -> *(x,*(y,z))
    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) -> *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(y,z)
     *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(x,*(y,z))
    Restore Modifier:
     DPs:
      +#(*(x,y),*(a(),y)) -> +#(x,a())
      +#(*(x,y),*(a(),y)) -> *#(+(x,a()),y)
      *#(*(x,y),z) -> *#(y,z)
      *#(*(x,y),z) -> *#(x,*(y,z))
     TRS:
      +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
      *(*(x,y),z) -> *(x,*(y,z))
     SCC Processor:
      #sccs: 1
      #rules: 2
      #arcs: 4/16
      DPs:
       *#(*(x,y),z) -> *#(y,z)
       *#(*(x,y),z) -> *#(x,*(y,z))
      TRS:
       +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
       *(*(x,y),z) -> *(x,*(y,z))
      Open