YES Time: 0.007 Problem: Equations: TRS: fAC(i(x),fAC(x,y)) -> y Proof: AC-KBO Processor: precedence: i > fAC weight function: [i](x0) = x0 + 15, [fAC](x0, x1) = x0 + x1 problem: Equations: TRS: Qed