YES Time: 0.727 Problem: Equations: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) TRS: +AC(a(),*AC(b(),c())) -> +AC(b(),f(*AC(a(),c()))) *AC(a(),+AC(b(),c())) -> *AC(b(),f(+AC(a(),c()))) Proof: DP Processor: Equations#: +{AC,#}(+AC(x0,x1),x2) -> +{AC,#}(x0,+AC(x1,x2)) +{AC,#}(x0,x1) -> +{AC,#}(x1,x0) *{AC,#}(*AC(x0,x1),x2) -> *{AC,#}(x0,*AC(x1,x2)) *{AC,#}(x0,x1) -> *{AC,#}(x1,x0) +{AC,#}(x0,+AC(x1,x2)) -> +{AC,#}(+AC(x0,x1),x2) +{AC,#}(x1,x0) -> +{AC,#}(x0,x1) *{AC,#}(x0,*AC(x1,x2)) -> *{AC,#}(*AC(x0,x1),x2) *{AC,#}(x1,x0) -> *{AC,#}(x0,x1) DPs: +{AC,#}(a(),*AC(b(),c())) -> *{AC,#}(a(),c()) +{AC,#}(a(),*AC(b(),c())) -> +{AC,#}(b(),f(*AC(a(),c()))) *{AC,#}(a(),+AC(b(),c())) -> +{AC,#}(a(),c()) *{AC,#}(a(),+AC(b(),c())) -> *{AC,#}(b(),f(+AC(a(),c()))) +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> *{AC,#}(a(),c()) +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> +{AC,#}(b(),f(*AC(a(),c()))) +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> +{AC,#}(x3,+AC(b(),f(*AC(a(),c())))) *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> +{AC,#}(a(),c()) *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> *{AC,#}(b(),f(+AC(a(),c()))) *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> *{AC,#}(x4,*AC(b(),f(+AC(a(),c())))) Equations: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) TRS: +AC(a(),*AC(b(),c())) -> +AC(b(),f(*AC(a(),c()))) *AC(a(),+AC(b(),c())) -> *AC(b(),f(+AC(a(),c()))) S: +{AC,#}(+AC(x5,x6),x7) -> +{AC,#}(x5,x6) +{AC,#}(x5,+AC(x6,x7)) -> +{AC,#}(x6,x7) *{AC,#}(*AC(x5,x6),x7) -> *{AC,#}(x5,x6) *{AC,#}(x5,*AC(x6,x7)) -> *{AC,#}(x6,x7) AC-EDG Processor: Equations#: +{AC,#}(+AC(x0,x1),x2) -> +{AC,#}(x0,+AC(x1,x2)) +{AC,#}(x0,x1) -> +{AC,#}(x1,x0) *{AC,#}(*AC(x0,x1),x2) -> *{AC,#}(x0,*AC(x1,x2)) *{AC,#}(x0,x1) -> *{AC,#}(x1,x0) +{AC,#}(x0,+AC(x1,x2)) -> +{AC,#}(+AC(x0,x1),x2) +{AC,#}(x1,x0) -> +{AC,#}(x0,x1) *{AC,#}(x0,*AC(x1,x2)) -> *{AC,#}(*AC(x0,x1),x2) *{AC,#}(x1,x0) -> *{AC,#}(x0,x1) DPs: +{AC,#}(a(),*AC(b(),c())) -> *{AC,#}(a(),c()) +{AC,#}(a(),*AC(b(),c())) -> +{AC,#}(b(),f(*AC(a(),c()))) *{AC,#}(a(),+AC(b(),c())) -> +{AC,#}(a(),c()) *{AC,#}(a(),+AC(b(),c())) -> *{AC,#}(b(),f(+AC(a(),c()))) +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> *{AC,#}(a(),c()) +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> +{AC,#}(b(),f(*AC(a(),c()))) +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> +{AC,#}(x3,+AC(b(),f(*AC(a(),c())))) *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> +{AC,#}(a(),c()) *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> *{AC,#}(b(),f(+AC(a(),c()))) *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> *{AC,#}(x4,*AC(b(),f(+AC(a(),c())))) Equations: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) TRS: +AC(a(),*AC(b(),c())) -> +AC(b(),f(*AC(a(),c()))) *AC(a(),+AC(b(),c())) -> *AC(b(),f(+AC(a(),c()))) S: +{AC,#}(+AC(x5,x6),x7) -> +{AC,#}(x5,x6) +{AC,#}(x5,+AC(x6,x7)) -> +{AC,#}(x6,x7) *{AC,#}(*AC(x5,x6),x7) -> *{AC,#}(x5,x6) *{AC,#}(x5,*AC(x6,x7)) -> *{AC,#}(x6,x7) SCC Processor: #sccs: 2 #rules: 2 #arcs: 10/100 Equations#: +{AC,#}(+AC(x0,x1),x2) -> +{AC,#}(x0,+AC(x1,x2)) +{AC,#}(x0,x1) -> +{AC,#}(x1,x0) *{AC,#}(*AC(x0,x1),x2) -> *{AC,#}(x0,*AC(x1,x2)) *{AC,#}(x0,x1) -> *{AC,#}(x1,x0) +{AC,#}(x0,+AC(x1,x2)) -> +{AC,#}(+AC(x0,x1),x2) +{AC,#}(x1,x0) -> +{AC,#}(x0,x1) *{AC,#}(x0,*AC(x1,x2)) -> *{AC,#}(*AC(x0,x1),x2) *{AC,#}(x1,x0) -> *{AC,#}(x0,x1) DPs: +{AC,#}(x3,+AC(a(),*AC(b(),c()))) -> +{AC,#}(x3,+AC(b(),f(*AC(a(),c())))) Equations: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) TRS: +AC(a(),*AC(b(),c())) -> +AC(b(),f(*AC(a(),c()))) *AC(a(),+AC(b(),c())) -> *AC(b(),f(+AC(a(),c()))) S: +{AC,#}(+AC(x5,x6),x7) -> +{AC,#}(x5,x6) +{AC,#}(x5,+AC(x6,x7)) -> +{AC,#}(x6,x7) *{AC,#}(*AC(x5,x6),x7) -> *{AC,#}(x5,x6) *{AC,#}(x5,*AC(x6,x7)) -> *{AC,#}(x6,x7) AC-DP unlabeling: Equations#: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) DPs: +AC(x3,+AC(a(),*AC(b(),c()))) -> +AC(x3,+AC(b(),f(*AC(a(),c())))) Equations: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) TRS: +AC(a(),*AC(b(),c())) -> +AC(b(),f(*AC(a(),c()))) *AC(a(),+AC(b(),c())) -> *AC(b(),f(+AC(a(),c()))) S: +AC(+AC(x5,x6),x7) -> +AC(x5,x6) +AC(x5,+AC(x6,x7)) -> +AC(x6,x7) *AC(*AC(x5,x6),x7) -> *AC(x5,x6) *AC(x5,*AC(x6,x7)) -> *AC(x6,x7) Usable Rule Processor: Equations#: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) DPs: +AC(x3,+AC(a(),*AC(b(),c()))) -> +AC(x3,+AC(b(),f(*AC(a(),c())))) Equations: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) TRS: S: +AC(+AC(x5,x6),x7) -> +AC(x5,x6) +AC(x5,+AC(x6,x7)) -> +AC(x6,x7) *AC(*AC(x5,x6),x7) -> *AC(x5,x6) *AC(x5,*AC(x6,x7)) -> *AC(x6,x7) AC-RPO Processor: argument filtering: pi(+AC) = [0,1] pi(*AC) = [0,1] pi(a) = [] pi(b) = [] pi(c) = [] pi(f) = 0 precedence: b > c > a > *AC > +AC > f status: problem: Equations#: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) DPs: Equations: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) TRS: S: +AC(+AC(x5,x6),x7) -> +AC(x5,x6) +AC(x5,+AC(x6,x7)) -> +AC(x6,x7) *AC(*AC(x5,x6),x7) -> *AC(x5,x6) *AC(x5,*AC(x6,x7)) -> *AC(x6,x7) Qed Equations#: +{AC,#}(+AC(x0,x1),x2) -> +{AC,#}(x0,+AC(x1,x2)) +{AC,#}(x0,x1) -> +{AC,#}(x1,x0) *{AC,#}(*AC(x0,x1),x2) -> *{AC,#}(x0,*AC(x1,x2)) *{AC,#}(x0,x1) -> *{AC,#}(x1,x0) +{AC,#}(x0,+AC(x1,x2)) -> +{AC,#}(+AC(x0,x1),x2) +{AC,#}(x1,x0) -> +{AC,#}(x0,x1) *{AC,#}(x0,*AC(x1,x2)) -> *{AC,#}(*AC(x0,x1),x2) *{AC,#}(x1,x0) -> *{AC,#}(x0,x1) DPs: *{AC,#}(x4,*AC(a(),+AC(b(),c()))) -> *{AC,#}(x4,*AC(b(),f(+AC(a(),c())))) Equations: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) TRS: +AC(a(),*AC(b(),c())) -> +AC(b(),f(*AC(a(),c()))) *AC(a(),+AC(b(),c())) -> *AC(b(),f(+AC(a(),c()))) S: +{AC,#}(+AC(x5,x6),x7) -> +{AC,#}(x5,x6) +{AC,#}(x5,+AC(x6,x7)) -> +{AC,#}(x6,x7) *{AC,#}(*AC(x5,x6),x7) -> *{AC,#}(x5,x6) *{AC,#}(x5,*AC(x6,x7)) -> *{AC,#}(x6,x7) AC-DP unlabeling: Equations#: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) DPs: *AC(x4,*AC(a(),+AC(b(),c()))) -> *AC(x4,*AC(b(),f(+AC(a(),c())))) Equations: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) TRS: +AC(a(),*AC(b(),c())) -> +AC(b(),f(*AC(a(),c()))) *AC(a(),+AC(b(),c())) -> *AC(b(),f(+AC(a(),c()))) S: +AC(+AC(x5,x6),x7) -> +AC(x5,x6) +AC(x5,+AC(x6,x7)) -> +AC(x6,x7) *AC(*AC(x5,x6),x7) -> *AC(x5,x6) *AC(x5,*AC(x6,x7)) -> *AC(x6,x7) Usable Rule Processor: Equations#: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) DPs: *AC(x4,*AC(a(),+AC(b(),c()))) -> *AC(x4,*AC(b(),f(+AC(a(),c())))) Equations: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) TRS: S: +AC(+AC(x5,x6),x7) -> +AC(x5,x6) +AC(x5,+AC(x6,x7)) -> +AC(x6,x7) *AC(*AC(x5,x6),x7) -> *AC(x5,x6) *AC(x5,*AC(x6,x7)) -> *AC(x6,x7) AC-RPO Processor: argument filtering: pi(+AC) = [] pi(*AC) = [0,1] pi(a) = [] pi(b) = [] pi(c) = [] pi(f) = [] precedence: a > +AC > f > *AC > b > c status: problem: Equations#: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) DPs: Equations: +AC(+AC(x0,x1),x2) -> +AC(x0,+AC(x1,x2)) +AC(x0,x1) -> +AC(x1,x0) *AC(*AC(x0,x1),x2) -> *AC(x0,*AC(x1,x2)) *AC(x0,x1) -> *AC(x1,x0) +AC(x0,+AC(x1,x2)) -> +AC(+AC(x0,x1),x2) +AC(x1,x0) -> +AC(x0,x1) *AC(x0,*AC(x1,x2)) -> *AC(*AC(x0,x1),x2) *AC(x1,x0) -> *AC(x0,x1) TRS: S: +AC(+AC(x5,x6),x7) -> +AC(x5,x6) +AC(x5,+AC(x6,x7)) -> +AC(x6,x7) *AC(*AC(x5,x6),x7) -> *AC(x5,x6) *AC(x5,*AC(x6,x7)) -> *AC(x6,x7) Qed