YES Time: 0.022 Problem: Equations: TRS: fAC(g(fAC(h(x),x)),x) -> fAC(h(x),fAC(x,x)) fAC(h(x),g(x)) -> fAC(g(h(x)),x) fAC(g(h(x)),fAC(x,fAC(x,y))) -> fAC(g(fAC(h(x),y)),x) fAC(g(g(x)),x) -> fAC(g(x),g(x)) Proof: AC-RPO Processor: precedence: h > fAC > g status: problem: Equations: TRS: Qed