YES Time: 0.009 Problem: Equations: fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3)) fAC(x1,x2) -> fAC(x2,x1) fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3) fAC(x2,x1) -> fAC(x1,x2) TRS: fAC(x,one()) -> x fAC(i(x),x) -> one() Proof: AC-RPO Processor: precedence: fAC > one > i status: problem: Equations: fAC(fAC(x1,x2),x3) -> fAC(x1,fAC(x2,x3)) fAC(x1,x2) -> fAC(x2,x1) fAC(x1,fAC(x2,x3)) -> fAC(fAC(x1,x2),x3) fAC(x2,x1) -> fAC(x1,x2) TRS: Qed