YES Time: 4.272 Problem: Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) Proof: DP Processor: Equations#: p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5)) p{AC,#}(x3,x4) -> p{AC,#}(x4,x3) m{AC,#}(mAC(x3,x4),x5) -> m{AC,#}(x3,mAC(x4,x5)) m{AC,#}(x3,x4) -> m{AC,#}(x4,x3) g{AC,#}(gAC(x3,x4),x5) -> g{AC,#}(x3,gAC(x4,x5)) g{AC,#}(x3,x4) -> g{AC,#}(x4,x3) p{AC,#}(x3,pAC(x4,x5)) -> p{AC,#}(pAC(x3,x4),x5) p{AC,#}(x4,x3) -> p{AC,#}(x3,x4) m{AC,#}(x3,mAC(x4,x5)) -> m{AC,#}(mAC(x3,x4),x5) m{AC,#}(x4,x3) -> m{AC,#}(x3,x4) g{AC,#}(x3,gAC(x4,x5)) -> g{AC,#}(gAC(x3,x4),x5) g{AC,#}(x4,x3) -> g{AC,#}(x3,x4) DPs: m{AC,#}(z,pAC(x,y)) -> m{AC,#}(z,y) m{AC,#}(z,pAC(x,y)) -> m{AC,#}(z,x) m{AC,#}(z,pAC(x,y)) -> p{AC,#}(mAC(z,x),mAC(z,y)) m{AC,#}(pAC(x,y),z) -> m{AC,#}(y,z) m{AC,#}(pAC(x,y),z) -> m{AC,#}(x,z) m{AC,#}(pAC(x,y),z) -> p{AC,#}(mAC(x,z),mAC(y,z)) sm#(x,sm(y,z)) -> m{AC,#}(x,y) sm#(x,sm(y,z)) -> sm#(mAC(x,y),z) g{AC,#}(sm(x,z),sm(y,z)) -> p{AC,#}(x,y) g{AC,#}(sm(x,z),sm(y,z)) -> sm#(pAC(x,y),z) sm#(x,gAC(y,z)) -> sm#(x,z) sm#(x,gAC(y,z)) -> sm#(x,y) sm#(x,gAC(y,z)) -> g{AC,#}(sm(x,y),sm(x,z)) smm#(x,smm(y,z)) -> m{AC,#}(x,y) smm#(x,smm(y,z)) -> smm#(mAC(x,y),z) g{AC,#}(smm(x,z),smm(y,z)) -> p{AC,#}(x,y) g{AC,#}(smm(x,z),smm(y,z)) -> smm#(pAC(x,y),z) smm#(x,gAC(y,z)) -> smm#(x,z) smm#(x,gAC(y,z)) -> smm#(x,y) smm#(x,gAC(y,z)) -> g{AC,#}(smm(x,y),smm(x,z)) p{AC,#}(x6,pAC(x,zero())) -> p{AC,#}(x6,x) p{AC,#}(x7,pAC(i(x),x)) -> p{AC,#}(x7,zero()) m{AC,#}(x8,mAC(one(),x)) -> m{AC,#}(x8,x) m{AC,#}(x9,mAC(x,one())) -> m{AC,#}(x9,x) m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(z,y) m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(z,x) m{AC,#}(x10,mAC(z,pAC(x,y))) -> p{AC,#}(mAC(z,x),mAC(z,y)) m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(x10,pAC(mAC(z,x),mAC(z,y))) m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(y,z) m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(x,z) m{AC,#}(x11,mAC(pAC(x,y),z)) -> p{AC,#}(mAC(x,z),mAC(y,z)) m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(x11,pAC(mAC(x,z),mAC(y,z))) g{AC,#}(x12,gAC(x,n())) -> g{AC,#}(x12,x) g{AC,#}(x13,gAC(x,inv(x))) -> g{AC,#}(x13,n()) g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> p{AC,#}(x,y) g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> sm#(pAC(x,y),z) g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> g{AC,#}(x14,sm(pAC(x,y),z)) g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> p{AC,#}(x,y) g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> smm#(pAC(x,y),z) g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> g{AC,#}(x15,smm(pAC(x,y),z)) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: p{AC,#}(pAC(x16,x17),x18) -> p{AC,#}(x16,x17) p{AC,#}(x16,pAC(x17,x18)) -> p{AC,#}(x17,x18) m{AC,#}(mAC(x16,x17),x18) -> m{AC,#}(x16,x17) m{AC,#}(x16,mAC(x17,x18)) -> m{AC,#}(x17,x18) g{AC,#}(gAC(x16,x17),x18) -> g{AC,#}(x16,x17) g{AC,#}(x16,gAC(x17,x18)) -> g{AC,#}(x17,x18) AC-EDG Processor: Equations#: p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5)) p{AC,#}(x3,x4) -> p{AC,#}(x4,x3) m{AC,#}(mAC(x3,x4),x5) -> m{AC,#}(x3,mAC(x4,x5)) m{AC,#}(x3,x4) -> m{AC,#}(x4,x3) g{AC,#}(gAC(x3,x4),x5) -> g{AC,#}(x3,gAC(x4,x5)) g{AC,#}(x3,x4) -> g{AC,#}(x4,x3) p{AC,#}(x3,pAC(x4,x5)) -> p{AC,#}(pAC(x3,x4),x5) p{AC,#}(x4,x3) -> p{AC,#}(x3,x4) m{AC,#}(x3,mAC(x4,x5)) -> m{AC,#}(mAC(x3,x4),x5) m{AC,#}(x4,x3) -> m{AC,#}(x3,x4) g{AC,#}(x3,gAC(x4,x5)) -> g{AC,#}(gAC(x3,x4),x5) g{AC,#}(x4,x3) -> g{AC,#}(x3,x4) DPs: m{AC,#}(z,pAC(x,y)) -> m{AC,#}(z,y) m{AC,#}(z,pAC(x,y)) -> m{AC,#}(z,x) m{AC,#}(z,pAC(x,y)) -> p{AC,#}(mAC(z,x),mAC(z,y)) m{AC,#}(pAC(x,y),z) -> m{AC,#}(y,z) m{AC,#}(pAC(x,y),z) -> m{AC,#}(x,z) m{AC,#}(pAC(x,y),z) -> p{AC,#}(mAC(x,z),mAC(y,z)) sm#(x,sm(y,z)) -> m{AC,#}(x,y) sm#(x,sm(y,z)) -> sm#(mAC(x,y),z) g{AC,#}(sm(x,z),sm(y,z)) -> p{AC,#}(x,y) g{AC,#}(sm(x,z),sm(y,z)) -> sm#(pAC(x,y),z) sm#(x,gAC(y,z)) -> sm#(x,z) sm#(x,gAC(y,z)) -> sm#(x,y) sm#(x,gAC(y,z)) -> g{AC,#}(sm(x,y),sm(x,z)) smm#(x,smm(y,z)) -> m{AC,#}(x,y) smm#(x,smm(y,z)) -> smm#(mAC(x,y),z) g{AC,#}(smm(x,z),smm(y,z)) -> p{AC,#}(x,y) g{AC,#}(smm(x,z),smm(y,z)) -> smm#(pAC(x,y),z) smm#(x,gAC(y,z)) -> smm#(x,z) smm#(x,gAC(y,z)) -> smm#(x,y) smm#(x,gAC(y,z)) -> g{AC,#}(smm(x,y),smm(x,z)) p{AC,#}(x6,pAC(x,zero())) -> p{AC,#}(x6,x) p{AC,#}(x7,pAC(i(x),x)) -> p{AC,#}(x7,zero()) m{AC,#}(x8,mAC(one(),x)) -> m{AC,#}(x8,x) m{AC,#}(x9,mAC(x,one())) -> m{AC,#}(x9,x) m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(z,y) m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(z,x) m{AC,#}(x10,mAC(z,pAC(x,y))) -> p{AC,#}(mAC(z,x),mAC(z,y)) m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(x10,pAC(mAC(z,x),mAC(z,y))) m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(y,z) m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(x,z) m{AC,#}(x11,mAC(pAC(x,y),z)) -> p{AC,#}(mAC(x,z),mAC(y,z)) m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(x11,pAC(mAC(x,z),mAC(y,z))) g{AC,#}(x12,gAC(x,n())) -> g{AC,#}(x12,x) g{AC,#}(x13,gAC(x,inv(x))) -> g{AC,#}(x13,n()) g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> p{AC,#}(x,y) g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> sm#(pAC(x,y),z) g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> g{AC,#}(x14,sm(pAC(x,y),z)) g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> p{AC,#}(x,y) g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> smm#(pAC(x,y),z) g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> g{AC,#}(x15,smm(pAC(x,y),z)) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: p{AC,#}(pAC(x16,x17),x18) -> p{AC,#}(x16,x17) p{AC,#}(x16,pAC(x17,x18)) -> p{AC,#}(x17,x18) m{AC,#}(mAC(x16,x17),x18) -> m{AC,#}(x16,x17) m{AC,#}(x16,mAC(x17,x18)) -> m{AC,#}(x17,x18) g{AC,#}(gAC(x16,x17),x18) -> g{AC,#}(x16,x17) g{AC,#}(x16,gAC(x17,x18)) -> g{AC,#}(x17,x18) SCC Processor: #sccs: 3 #rules: 30 #arcs: 366/1600 Equations#: p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5)) p{AC,#}(x3,x4) -> p{AC,#}(x4,x3) m{AC,#}(mAC(x3,x4),x5) -> m{AC,#}(x3,mAC(x4,x5)) m{AC,#}(x3,x4) -> m{AC,#}(x4,x3) g{AC,#}(gAC(x3,x4),x5) -> g{AC,#}(x3,gAC(x4,x5)) g{AC,#}(x3,x4) -> g{AC,#}(x4,x3) p{AC,#}(x3,pAC(x4,x5)) -> p{AC,#}(pAC(x3,x4),x5) p{AC,#}(x4,x3) -> p{AC,#}(x3,x4) m{AC,#}(x3,mAC(x4,x5)) -> m{AC,#}(mAC(x3,x4),x5) m{AC,#}(x4,x3) -> m{AC,#}(x3,x4) g{AC,#}(x3,gAC(x4,x5)) -> g{AC,#}(gAC(x3,x4),x5) g{AC,#}(x4,x3) -> g{AC,#}(x3,x4) DPs: smm#(x,smm(y,z)) -> smm#(mAC(x,y),z) smm#(x,gAC(y,z)) -> g{AC,#}(smm(x,y),smm(x,z)) g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> g{AC,#}(x15,smm(pAC(x,y),z)) g{AC,#}(x15,gAC(smm(x,z),smm(y,z))) -> smm#(pAC(x,y),z) smm#(x,gAC(y,z)) -> smm#(x,y) smm#(x,gAC(y,z)) -> smm#(x,z) g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> g{AC,#}(x14,sm(pAC(x,y),z)) g{AC,#}(x14,gAC(sm(x,z),sm(y,z))) -> sm#(pAC(x,y),z) sm#(x,gAC(y,z)) -> g{AC,#}(sm(x,y),sm(x,z)) g{AC,#}(x13,gAC(x,inv(x))) -> g{AC,#}(x13,n()) g{AC,#}(x12,gAC(x,n())) -> g{AC,#}(x12,x) g{AC,#}(smm(x,z),smm(y,z)) -> smm#(pAC(x,y),z) g{AC,#}(sm(x,z),sm(y,z)) -> sm#(pAC(x,y),z) sm#(x,gAC(y,z)) -> sm#(x,y) sm#(x,gAC(y,z)) -> sm#(x,z) sm#(x,sm(y,z)) -> sm#(mAC(x,y),z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: p{AC,#}(pAC(x16,x17),x18) -> p{AC,#}(x16,x17) p{AC,#}(x16,pAC(x17,x18)) -> p{AC,#}(x17,x18) m{AC,#}(mAC(x16,x17),x18) -> m{AC,#}(x16,x17) m{AC,#}(x16,mAC(x17,x18)) -> m{AC,#}(x17,x18) g{AC,#}(gAC(x16,x17),x18) -> g{AC,#}(x16,x17) g{AC,#}(x16,gAC(x17,x18)) -> g{AC,#}(x17,x18) AC-DP unlabeling: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: smm#(x,smm(y,z)) -> smm#(mAC(x,y),z) smm#(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) gAC(x15,gAC(smm(x,z),smm(y,z))) -> gAC(x15,smm(pAC(x,y),z)) gAC(x15,gAC(smm(x,z),smm(y,z))) -> smm#(pAC(x,y),z) smm#(x,gAC(y,z)) -> smm#(x,y) smm#(x,gAC(y,z)) -> smm#(x,z) gAC(x14,gAC(sm(x,z),sm(y,z))) -> gAC(x14,sm(pAC(x,y),z)) gAC(x14,gAC(sm(x,z),sm(y,z))) -> sm#(pAC(x,y),z) sm#(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) gAC(x13,gAC(x,inv(x))) -> gAC(x13,n()) gAC(x12,gAC(x,n())) -> gAC(x12,x) gAC(smm(x,z),smm(y,z)) -> smm#(pAC(x,y),z) gAC(sm(x,z),sm(y,z)) -> sm#(pAC(x,y),z) sm#(x,gAC(y,z)) -> sm#(x,y) sm#(x,gAC(y,z)) -> sm#(x,z) sm#(x,sm(y,z)) -> sm#(mAC(x,y),z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) AC-RPO Processor: argument filtering: pi(pAC) = [0,1] pi(gAC) = [0,1] pi(mAC) = [0,1] pi(zero) = [] pi(i) = [] pi(one) = [] pi(n) = [] pi(inv) = [] pi(sm) = 1 pi(smm) = 1 pi(sm#) = [1] pi(smm#) = [1] precedence: mAC > inv > gAC > one > zero > n > smm# > sm > pAC > i > smm > sm# status: smm#:mul sm#:mul smm:mul sm:mul problem: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: smm#(x,smm(y,z)) -> smm#(mAC(x,y),z) sm#(x,sm(y,z)) -> sm#(mAC(x,y),z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) Restore Modifier: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: smm#(x,smm(y,z)) -> smm#(mAC(x,y),z) sm#(x,sm(y,z)) -> sm#(mAC(x,y),z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) SCC Processor: #sccs: 2 #rules: 2 #arcs: 88/4 Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: sm#(x,sm(y,z)) -> sm#(mAC(x,y),z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) AC-DP unlabeling: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: sm#(x,sm(y,z)) -> sm#(mAC(x,y),z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) Usable Rule Processor: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: sm#(x,sm(y,z)) -> sm#(mAC(x,y),z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) pAC(x,zero()) -> x pAC(i(x),x) -> zero() S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) AC-RPO Processor: argument filtering: pi(pAC) = [] pi(gAC) = [] pi(mAC) = [] pi(zero) = [] pi(i) = 0 pi(one) = [] pi(sm) = [0,1] pi(sm#) = [1] precedence: sm > sm# > one > zero > i > mAC > gAC > pAC status: sm#:lex sm:mul problem: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) pAC(x,zero()) -> x pAC(i(x),x) -> zero() S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) Qed Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: smm#(x,smm(y,z)) -> smm#(mAC(x,y),z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) AC-DP unlabeling: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: smm#(x,smm(y,z)) -> smm#(mAC(x,y),z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) Usable Rule Processor: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: smm#(x,smm(y,z)) -> smm#(mAC(x,y),z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) pAC(x,zero()) -> x pAC(i(x),x) -> zero() S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) AC-RPO Processor: argument filtering: pi(pAC) = [] pi(gAC) = [] pi(mAC) = [] pi(zero) = [] pi(i) = 0 pi(one) = [] pi(smm) = [0,1] pi(smm#) = [1] precedence: smm > smm# > one > zero > i > mAC > gAC > pAC status: smm#:lex smm:mul problem: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) pAC(x,zero()) -> x pAC(i(x),x) -> zero() S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) Qed Equations#: p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5)) p{AC,#}(x3,x4) -> p{AC,#}(x4,x3) m{AC,#}(mAC(x3,x4),x5) -> m{AC,#}(x3,mAC(x4,x5)) m{AC,#}(x3,x4) -> m{AC,#}(x4,x3) g{AC,#}(gAC(x3,x4),x5) -> g{AC,#}(x3,gAC(x4,x5)) g{AC,#}(x3,x4) -> g{AC,#}(x4,x3) p{AC,#}(x3,pAC(x4,x5)) -> p{AC,#}(pAC(x3,x4),x5) p{AC,#}(x4,x3) -> p{AC,#}(x3,x4) m{AC,#}(x3,mAC(x4,x5)) -> m{AC,#}(mAC(x3,x4),x5) m{AC,#}(x4,x3) -> m{AC,#}(x3,x4) g{AC,#}(x3,gAC(x4,x5)) -> g{AC,#}(gAC(x3,x4),x5) g{AC,#}(x4,x3) -> g{AC,#}(x3,x4) DPs: m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(x11,pAC(mAC(x,z),mAC(y,z))) m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(x,z) m{AC,#}(x11,mAC(pAC(x,y),z)) -> m{AC,#}(y,z) m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(x10,pAC(mAC(z,x),mAC(z,y))) m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(z,x) m{AC,#}(x10,mAC(z,pAC(x,y))) -> m{AC,#}(z,y) m{AC,#}(x9,mAC(x,one())) -> m{AC,#}(x9,x) m{AC,#}(x8,mAC(one(),x)) -> m{AC,#}(x8,x) m{AC,#}(pAC(x,y),z) -> m{AC,#}(x,z) m{AC,#}(pAC(x,y),z) -> m{AC,#}(y,z) m{AC,#}(z,pAC(x,y)) -> m{AC,#}(z,x) m{AC,#}(z,pAC(x,y)) -> m{AC,#}(z,y) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: p{AC,#}(pAC(x16,x17),x18) -> p{AC,#}(x16,x17) p{AC,#}(x16,pAC(x17,x18)) -> p{AC,#}(x17,x18) m{AC,#}(mAC(x16,x17),x18) -> m{AC,#}(x16,x17) m{AC,#}(x16,mAC(x17,x18)) -> m{AC,#}(x17,x18) g{AC,#}(gAC(x16,x17),x18) -> g{AC,#}(x16,x17) g{AC,#}(x16,gAC(x17,x18)) -> g{AC,#}(x17,x18) AC-DP unlabeling: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: mAC(x11,mAC(pAC(x,y),z)) -> mAC(x11,pAC(mAC(x,z),mAC(y,z))) mAC(x11,mAC(pAC(x,y),z)) -> mAC(x,z) mAC(x11,mAC(pAC(x,y),z)) -> mAC(y,z) mAC(x10,mAC(z,pAC(x,y))) -> mAC(x10,pAC(mAC(z,x),mAC(z,y))) mAC(x10,mAC(z,pAC(x,y))) -> mAC(z,x) mAC(x10,mAC(z,pAC(x,y))) -> mAC(z,y) mAC(x9,mAC(x,one())) -> mAC(x9,x) mAC(x8,mAC(one(),x)) -> mAC(x8,x) mAC(pAC(x,y),z) -> mAC(x,z) mAC(pAC(x,y),z) -> mAC(y,z) mAC(z,pAC(x,y)) -> mAC(z,x) mAC(z,pAC(x,y)) -> mAC(z,y) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) Usable Rule Processor: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: mAC(x11,mAC(pAC(x,y),z)) -> mAC(x11,pAC(mAC(x,z),mAC(y,z))) mAC(x11,mAC(pAC(x,y),z)) -> mAC(x,z) mAC(x11,mAC(pAC(x,y),z)) -> mAC(y,z) mAC(x10,mAC(z,pAC(x,y))) -> mAC(x10,pAC(mAC(z,x),mAC(z,y))) mAC(x10,mAC(z,pAC(x,y))) -> mAC(z,x) mAC(x10,mAC(z,pAC(x,y))) -> mAC(z,y) mAC(x9,mAC(x,one())) -> mAC(x9,x) mAC(x8,mAC(one(),x)) -> mAC(x8,x) mAC(pAC(x,y),z) -> mAC(x,z) mAC(pAC(x,y),z) -> mAC(y,z) mAC(z,pAC(x,y)) -> mAC(z,x) mAC(z,pAC(x,y)) -> mAC(z,y) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) pAC(x,zero()) -> x pAC(i(x),x) -> zero() S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) AC-RPO Processor: argument filtering: pi(pAC) = [0,1] pi(gAC) = [] pi(mAC) = [0,1] pi(zero) = [] pi(i) = [] pi(one) = [] precedence: mAC > i > pAC > zero > gAC > one status: problem: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) pAC(x,zero()) -> x pAC(i(x),x) -> zero() S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) Qed Equations#: p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5)) p{AC,#}(x3,x4) -> p{AC,#}(x4,x3) m{AC,#}(mAC(x3,x4),x5) -> m{AC,#}(x3,mAC(x4,x5)) m{AC,#}(x3,x4) -> m{AC,#}(x4,x3) g{AC,#}(gAC(x3,x4),x5) -> g{AC,#}(x3,gAC(x4,x5)) g{AC,#}(x3,x4) -> g{AC,#}(x4,x3) p{AC,#}(x3,pAC(x4,x5)) -> p{AC,#}(pAC(x3,x4),x5) p{AC,#}(x4,x3) -> p{AC,#}(x3,x4) m{AC,#}(x3,mAC(x4,x5)) -> m{AC,#}(mAC(x3,x4),x5) m{AC,#}(x4,x3) -> m{AC,#}(x3,x4) g{AC,#}(x3,gAC(x4,x5)) -> g{AC,#}(gAC(x3,x4),x5) g{AC,#}(x4,x3) -> g{AC,#}(x3,x4) DPs: p{AC,#}(x7,pAC(i(x),x)) -> p{AC,#}(x7,zero()) p{AC,#}(x6,pAC(x,zero())) -> p{AC,#}(x6,x) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: p{AC,#}(pAC(x16,x17),x18) -> p{AC,#}(x16,x17) p{AC,#}(x16,pAC(x17,x18)) -> p{AC,#}(x17,x18) m{AC,#}(mAC(x16,x17),x18) -> m{AC,#}(x16,x17) m{AC,#}(x16,mAC(x17,x18)) -> m{AC,#}(x17,x18) g{AC,#}(gAC(x16,x17),x18) -> g{AC,#}(x16,x17) g{AC,#}(x16,gAC(x17,x18)) -> g{AC,#}(x17,x18) AC-DP unlabeling: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: pAC(x7,pAC(i(x),x)) -> pAC(x7,zero()) pAC(x6,pAC(x,zero())) -> pAC(x6,x) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() mAC(one(),x) -> x mAC(x,one()) -> x mAC(z,pAC(x,y)) -> pAC(mAC(z,x),mAC(z,y)) mAC(pAC(x,y),z) -> pAC(mAC(x,z),mAC(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(mAC(x,y),z) sm(one(),z) -> z gAC(sm(x,z),sm(y,z)) -> sm(pAC(x,y),z) sm(x,gAC(y,z)) -> gAC(sm(x,y),sm(x,z)) smm(x,smm(y,z)) -> smm(mAC(x,y),z) smm(one(),z) -> z gAC(smm(x,z),smm(y,z)) -> smm(pAC(x,y),z) smm(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) Usable Rule Processor: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: pAC(x7,pAC(i(x),x)) -> pAC(x7,zero()) pAC(x6,pAC(x,zero())) -> pAC(x6,x) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) AC-RPO Processor: argument filtering: pi(pAC) = [0,1] pi(gAC) = [0,1] pi(mAC) = [] pi(zero) = [] pi(i) = [] precedence: pAC > i > zero > mAC > gAC status: problem: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(x4,x3) mAC(mAC(x3,x4),x5) -> mAC(x3,mAC(x4,x5)) mAC(x3,x4) -> mAC(x4,x3) gAC(gAC(x3,x4),x5) -> gAC(x3,gAC(x4,x5)) gAC(x3,x4) -> gAC(x4,x3) pAC(x3,pAC(x4,x5)) -> pAC(pAC(x3,x4),x5) pAC(x4,x3) -> pAC(x3,x4) mAC(x3,mAC(x4,x5)) -> mAC(mAC(x3,x4),x5) mAC(x4,x3) -> mAC(x3,x4) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: pAC(x,zero()) -> x pAC(i(x),x) -> zero() S: pAC(pAC(x16,x17),x18) -> pAC(x16,x17) pAC(x16,pAC(x17,x18)) -> pAC(x17,x18) mAC(mAC(x16,x17),x18) -> mAC(x16,x17) mAC(x16,mAC(x17,x18)) -> mAC(x17,x18) gAC(gAC(x16,x17),x18) -> gAC(x16,x17) gAC(x16,gAC(x17,x18)) -> gAC(x17,x18) Qed