YES Time: 0.016 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: fAC > g > h weight function: w0 = 2 w(h) = 3 w(g) = 1 w(fAC) = 0 problem: Equations: TRS: Qed