YES Time: 0.010 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(x,x) -> x Proof: AC-KBO Processor: precedence: one ~ fAC weight function: w0 = 4 w(one) = 4 w(fAC) = 0 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