YES Time: 0.120 Problem: Equations: TRS: fAC(g(g(x)),x) -> fAC(g(x),g(x)) fAC(fAC(x,x),g(x)) -> fAC(x,h(x)) Proof: AC-KBO Processor: precedence: h > g > fAC weight function: [h](x0) = 2x0 + 2, [g](x0) = x0 + 2, [fAC](x0, x1) = x0 + x1 + 1 problem: Equations: TRS: Qed