YES Time: 0.044 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: DP Processor: Equations#: f{AC,#}(fAC(x1,x2),x3) -> f{AC,#}(x1,fAC(x2,x3)) f{AC,#}(x1,x2) -> f{AC,#}(x2,x1) f{AC,#}(x1,fAC(x2,x3)) -> f{AC,#}(fAC(x1,x2),x3) f{AC,#}(x2,x1) -> f{AC,#}(x1,x2) DPs: f{AC,#}(x4,fAC(x,one())) -> f{AC,#}(x4,x) f{AC,#}(x5,fAC(i(x),x)) -> f{AC,#}(x5,one()) 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() S: f{AC,#}(fAC(x6,x7),x8) -> f{AC,#}(x6,x7) f{AC,#}(x6,fAC(x7,x8)) -> f{AC,#}(x7,x8) AC-DP unlabeling: 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) DPs: fAC(x4,fAC(x,one())) -> fAC(x4,x) fAC(x5,fAC(i(x),x)) -> fAC(x5,one()) 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() S: fAC(fAC(x6,x7),x8) -> fAC(x6,x7) fAC(x6,fAC(x7,x8)) -> fAC(x7,x8) AC-KBO Processor: argument filtering: pi(fAC) = [0,1] pi(one) = [] pi(i) = [] precedence: fAC > i ~ one weight function: w0 = 1 w(fAC) = 7 w(i) = w(one) = 1 usable rules: fAC(x,one()) -> x fAC(i(x),x) -> one() 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) DPs: 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() S: fAC(fAC(x6,x7),x8) -> fAC(x6,x7) fAC(x6,fAC(x7,x8)) -> fAC(x7,x8) Qed