YES Time: 0.013 Problem: Equations: TRS: fAC(hAC(g(g(x)),x),g(fAC(x,y))) -> fAC(hAC(g(x),g(x)),fAC(g(x),y)) hAC(fAC(x,y),x) -> fAC(hAC(x,y),x) fAC(g(x),y) -> g(fAC(x,y)) Proof: AC-KBO Processor: precedence: hAC > fAC > g weight function: w0 = 8 w(g) = 6 w(hAC) = w(fAC) = 0 problem: Equations: TRS: Qed