YES Time: 0.112 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) = 8x0 + 5, [g](x0) = 8x0 + 1, [fAC](x0, x1) = x0 + x1 + 5 problem: Equations: TRS: Qed