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