YES Time: 0.011 Problem: Equations: TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) Proof: AC-RPO Processor: precedence: plusAC > s > 0 status: problem: Equations: TRS: Qed