YES
Time: 0.015

Problem:
 Equations:
  
 TRS:
  s(p(x)) -> x
  p(s(x)) -> x
  minus(x,0()) -> x
  minus(x,s(y)) -> p(minus(x,y))
  minus(x,p(y)) -> s(minus(x,y))
  plusAC(x,0()) -> x
  plusAC(x,s(y)) -> s(plusAC(x,y))
  plusAC(x,p(y)) -> p(plusAC(x,y))

Proof:
 AC-KBO Processor:
  precedence:
   minus ~ plusAC > 0 ~ s ~ p
   weight function:
    w0 = 8
    w(s) = w(p) = 15
    w(0) = 8
    w(minus) = w(plusAC) = 0
   problem:
    Equations:
     
    TRS:
     
   Qed