YES Time: 0.039 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(b(),fAC(b(),b()))) -> fAC(g(fAC(h(a()),a())),a()) fAC(h(a()),a()) -> fAC(h(a()),b()) Proof: AC-KBO Processor: precedence: h > fAC > a > b > g weight function: w0 = 1 w(g) = 11 w(h) = 9 w(fAC) = 6 w(a) = 2 w(b) = 1 problem: Equations: TRS: Qed