YES Time: 0.013 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-KBO Processor: precedence: fAC > i ~ one weight function: w0 = 2 w(one) = 6 w(i) = 2 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