YES Time: 0.008 Problem: Equations: TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) Proof: AC-KBO Processor: precedence: 0 > plusAC > s weight function: w0 = 8 w(s) = 15 w(0) = 8 w(plusAC) = 0 problem: Equations: TRS: Qed