MAYBE

Problem:
 p(s(x)) -> x
 s(p(x)) -> x
 +(0(),y) -> y
 +(s(x),y) -> s(+(x,y))
 +(p(x),y) -> p(+(x,y))
 minus(0()) -> 0()
 minus(s(x)) -> p(minus(x))
 minus(p(x)) -> s(minus(x))
 *(0(),y) -> 0()
 *(s(x),y) -> +(*(x,y),y)
 *(p(x),y) -> +(*(x,y),minus(y))

Proof:
 DP Processor:
  DPs:
   +#(s(x),y) -> +#(x,y)
   +#(s(x),y) -> s#(+(x,y))
   +#(p(x),y) -> +#(x,y)
   +#(p(x),y) -> p#(+(x,y))
   minus#(s(x)) -> minus#(x)
   minus#(s(x)) -> p#(minus(x))
   minus#(p(x)) -> minus#(x)
   minus#(p(x)) -> s#(minus(x))
   *#(s(x),y) -> *#(x,y)
   *#(s(x),y) -> +#(*(x,y),y)
   *#(p(x),y) -> minus#(y)
   *#(p(x),y) -> *#(x,y)
   *#(p(x),y) -> +#(*(x,y),minus(y))
  TRS:
   p(s(x)) -> x
   s(p(x)) -> x
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   +(p(x),y) -> p(+(x,y))
   minus(0()) -> 0()
   minus(s(x)) -> p(minus(x))
   minus(p(x)) -> s(minus(x))
   *(0(),y) -> 0()
   *(s(x),y) -> +(*(x,y),y)
   *(p(x),y) -> +(*(x,y),minus(y))
  Open