YES Time: 0.033 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-KBO Processor: precedence: i > h > a > b > fAC > g weight function: w0 = 1 w(h) = 14 w(a) = 2 w(b) = w(g) = 1 w(i) = w(fAC) = 0 problem: Equations: TRS: Qed