YES Time: 1.601 Problem: Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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) 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) g{AC,#}(x3,gAC(x4,x5)) -> g{AC,#}(gAC(x3,x4),x5) g{AC,#}(x4,x3) -> g{AC,#}(x3,x4) DPs: m#(x,m(y,z)) -> m#(x,y) m#(x,m(y,z)) -> m#(m(x,y),z) m#(z,pAC(x,y)) -> m#(z,y) m#(z,pAC(x,y)) -> m#(z,x) m#(z,pAC(x,y)) -> p{AC,#}(m(z,x),m(z,y)) m#(pAC(x,y),z) -> m#(y,z) m#(pAC(x,y),z) -> m#(x,z) m#(pAC(x,y),z) -> p{AC,#}(m(x,z),m(y,z)) sm#(x,sm(y,z)) -> m#(x,y) sm#(x,sm(y,z)) -> sm#(m(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#(x,y) smm#(x,smm(y,z)) -> smm#(m(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()) g{AC,#}(x8,gAC(x,n())) -> g{AC,#}(x8,x) g{AC,#}(x9,gAC(x,inv(x))) -> g{AC,#}(x9,n()) g{AC,#}(x10,gAC(sm(x,z),sm(y,z))) -> p{AC,#}(x,y) g{AC,#}(x10,gAC(sm(x,z),sm(y,z))) -> sm#(pAC(x,y),z) g{AC,#}(x10,gAC(sm(x,z),sm(y,z))) -> g{AC,#}(x10,sm(pAC(x,y),z)) g{AC,#}(x11,gAC(smm(x,z),smm(y,z))) -> p{AC,#}(x,y) g{AC,#}(x11,gAC(smm(x,z),smm(y,z))) -> smm#(pAC(x,y),z) g{AC,#}(x11,gAC(smm(x,z),smm(y,z))) -> g{AC,#}(x11,smm(pAC(x,y),z)) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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(x12,x13),x14) -> p{AC,#}(x12,x13) p{AC,#}(x12,pAC(x13,x14)) -> p{AC,#}(x13,x14) g{AC,#}(gAC(x12,x13),x14) -> g{AC,#}(x12,x13) g{AC,#}(x12,gAC(x13,x14)) -> g{AC,#}(x13,x14) AC-EDG Processor: Equations#: p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5)) p{AC,#}(x3,x4) -> p{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) g{AC,#}(x3,gAC(x4,x5)) -> g{AC,#}(gAC(x3,x4),x5) g{AC,#}(x4,x3) -> g{AC,#}(x3,x4) DPs: m#(x,m(y,z)) -> m#(x,y) m#(x,m(y,z)) -> m#(m(x,y),z) m#(z,pAC(x,y)) -> m#(z,y) m#(z,pAC(x,y)) -> m#(z,x) m#(z,pAC(x,y)) -> p{AC,#}(m(z,x),m(z,y)) m#(pAC(x,y),z) -> m#(y,z) m#(pAC(x,y),z) -> m#(x,z) m#(pAC(x,y),z) -> p{AC,#}(m(x,z),m(y,z)) sm#(x,sm(y,z)) -> m#(x,y) sm#(x,sm(y,z)) -> sm#(m(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#(x,y) smm#(x,smm(y,z)) -> smm#(m(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()) g{AC,#}(x8,gAC(x,n())) -> g{AC,#}(x8,x) g{AC,#}(x9,gAC(x,inv(x))) -> g{AC,#}(x9,n()) g{AC,#}(x10,gAC(sm(x,z),sm(y,z))) -> p{AC,#}(x,y) g{AC,#}(x10,gAC(sm(x,z),sm(y,z))) -> sm#(pAC(x,y),z) g{AC,#}(x10,gAC(sm(x,z),sm(y,z))) -> g{AC,#}(x10,sm(pAC(x,y),z)) g{AC,#}(x11,gAC(smm(x,z),smm(y,z))) -> p{AC,#}(x,y) g{AC,#}(x11,gAC(smm(x,z),smm(y,z))) -> smm#(pAC(x,y),z) g{AC,#}(x11,gAC(smm(x,z),smm(y,z))) -> g{AC,#}(x11,smm(pAC(x,y),z)) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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(x12,x13),x14) -> p{AC,#}(x12,x13) p{AC,#}(x12,pAC(x13,x14)) -> p{AC,#}(x13,x14) g{AC,#}(gAC(x12,x13),x14) -> g{AC,#}(x12,x13) g{AC,#}(x12,gAC(x13,x14)) -> g{AC,#}(x13,x14) SCC Processor: #sccs: 3 #rules: 24 #arcs: 202/1024 Equations#: p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5)) p{AC,#}(x3,x4) -> p{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) 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#(m(x,y),z) smm#(x,gAC(y,z)) -> g{AC,#}(smm(x,y),smm(x,z)) g{AC,#}(x11,gAC(smm(x,z),smm(y,z))) -> g{AC,#}(x11,smm(pAC(x,y),z)) g{AC,#}(x11,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,#}(x10,gAC(sm(x,z),sm(y,z))) -> g{AC,#}(x10,sm(pAC(x,y),z)) g{AC,#}(x10,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,#}(x9,gAC(x,inv(x))) -> g{AC,#}(x9,n()) g{AC,#}(x8,gAC(x,n())) -> g{AC,#}(x8,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#(m(x,y),z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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(x12,x13),x14) -> p{AC,#}(x12,x13) p{AC,#}(x12,pAC(x13,x14)) -> p{AC,#}(x13,x14) g{AC,#}(gAC(x12,x13),x14) -> g{AC,#}(x12,x13) g{AC,#}(x12,gAC(x13,x14)) -> g{AC,#}(x13,x14) AC-DP unlabeling: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: smm#(x,smm(y,z)) -> smm#(m(x,y),z) smm#(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) gAC(x11,gAC(smm(x,z),smm(y,z))) -> gAC(x11,smm(pAC(x,y),z)) gAC(x11,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(x10,gAC(sm(x,z),sm(y,z))) -> gAC(x10,sm(pAC(x,y),z)) gAC(x10,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(x9,gAC(x,inv(x))) -> gAC(x9,n()) gAC(x8,gAC(x,n())) -> gAC(x8,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#(m(x,y),z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) AC-KBO Processor: argument filtering: pi(pAC) = [0,1] pi(gAC) = [0,1] pi(zero) = [] pi(i) = [] pi(one) = [] pi(m) = [1] pi(n) = [] pi(inv) = [0] pi(sm) = [1] pi(smm) = 1 pi(sm#) = [1] pi(smm#) = 1 precedence: smm# ~ sm# ~ sm ~ inv ~ n ~ m ~ one ~ i ~ zero ~ pAC > gAC > smm weight function: w0 = 1 w(pAC) = 7 w(inv) = 5 w(m) = w(zero) = 4 w(n) = 2 w(smm#) = w(smm) = w(one) = w(i) = 1 w(sm#) = w(sm) = w(gAC) = 0 usable rules: gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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)) problem: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: smm#(x,smm(y,z)) -> smm#(m(x,y),z) smm#(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) Restore Modifier: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: smm#(x,smm(y,z)) -> smm#(m(x,y),z) smm#(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) AC-DP unlabeling: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: smm#(x,smm(y,z)) -> smm#(m(x,y),z) smm#(x,gAC(y,z)) -> gAC(smm(x,y),smm(x,z)) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) AC-KBO Processor: argument filtering: pi(pAC) = [0,1] pi(gAC) = [0,1] pi(zero) = [] pi(i) = 0 pi(one) = [] pi(m) = 0 pi(n) = [] pi(inv) = 0 pi(sm) = 1 pi(smm) = [1] pi(smm#) = [1] precedence: smm# ~ smm ~ m ~ one ~ zero ~ pAC > gAC > sm ~ inv ~ n ~ i weight function: w0 = 1 w(i) = 6 w(one) = 4 w(pAC) = 3 w(n) = 2 w(smm#) = w(inv) = w(m) = w(zero) = 1 w(smm) = w(sm) = w(gAC) = 0 usable rules: gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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)) problem: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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) 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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) Qed Equations#: p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5)) p{AC,#}(x3,x4) -> p{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) g{AC,#}(x3,gAC(x4,x5)) -> g{AC,#}(gAC(x3,x4),x5) g{AC,#}(x4,x3) -> g{AC,#}(x3,x4) DPs: m#(pAC(x,y),z) -> m#(x,z) m#(pAC(x,y),z) -> m#(y,z) m#(z,pAC(x,y)) -> m#(z,x) m#(z,pAC(x,y)) -> m#(z,y) m#(x,m(y,z)) -> m#(m(x,y),z) m#(x,m(y,z)) -> m#(x,y) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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(x12,x13),x14) -> p{AC,#}(x12,x13) p{AC,#}(x12,pAC(x13,x14)) -> p{AC,#}(x13,x14) g{AC,#}(gAC(x12,x13),x14) -> g{AC,#}(x12,x13) g{AC,#}(x12,gAC(x13,x14)) -> g{AC,#}(x13,x14) AC-DP unlabeling: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: m#(pAC(x,y),z) -> m#(x,z) m#(pAC(x,y),z) -> m#(y,z) m#(z,pAC(x,y)) -> m#(z,x) m#(z,pAC(x,y)) -> m#(z,y) m#(x,m(y,z)) -> m#(m(x,y),z) m#(x,m(y,z)) -> m#(x,y) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) Usable Rule Processor: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: m#(pAC(x,y),z) -> m#(x,z) m#(pAC(x,y),z) -> m#(y,z) m#(z,pAC(x,y)) -> m#(z,x) m#(z,pAC(x,y)) -> m#(z,y) m#(x,m(y,z)) -> m#(m(x,y),z) m#(x,m(y,z)) -> m#(x,y) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) pAC(x,zero()) -> x pAC(i(x),x) -> zero() S: pAC(pAC(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) AC-KBO Processor: argument filtering: pi(pAC) = [0,1] pi(zero) = [] pi(i) = [] pi(one) = [] pi(m) = [0,1] pi(m#) = 1 precedence: m# ~ m ~ one ~ i ~ zero ~ pAC weight function: w0 = 3 w(m) = w(i) = 6 w(one) = w(zero) = 4 w(pAC) = 2 w(m#) = 1 usable rules: problem: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: m#(pAC(x,y),z) -> m#(x,z) m#(pAC(x,y),z) -> m#(y,z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) pAC(x,zero()) -> x pAC(i(x),x) -> zero() S: pAC(pAC(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) Restore Modifier: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: m#(pAC(x,y),z) -> m#(x,z) m#(pAC(x,y),z) -> m#(y,z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) pAC(x,zero()) -> x pAC(i(x),x) -> zero() S: pAC(pAC(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) AC-DP unlabeling: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: m#(pAC(x,y),z) -> m#(x,z) m#(pAC(x,y),z) -> m#(y,z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) pAC(x,zero()) -> x pAC(i(x),x) -> zero() S: pAC(pAC(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) Usable Rule Processor: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) DPs: m#(pAC(x,y),z) -> m#(x,z) m#(pAC(x,y),z) -> m#(y,z) Equations: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: S: pAC(pAC(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) AC-KBO Processor: argument filtering: pi(pAC) = [0,1] pi(m#) = [0,1] precedence: m# ~ pAC weight function: w0 = 6 w(m#) = 6 w(pAC) = 4 usable rules: problem: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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) 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) gAC(x3,gAC(x4,x5)) -> gAC(gAC(x3,x4),x5) gAC(x4,x3) -> gAC(x3,x4) TRS: S: pAC(pAC(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) Qed Equations#: p{AC,#}(pAC(x3,x4),x5) -> p{AC,#}(x3,pAC(x4,x5)) p{AC,#}(x3,x4) -> p{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) 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) 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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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(x12,x13),x14) -> p{AC,#}(x12,x13) p{AC,#}(x12,pAC(x13,x14)) -> p{AC,#}(x13,x14) g{AC,#}(gAC(x12,x13),x14) -> g{AC,#}(x12,x13) g{AC,#}(x12,gAC(x13,x14)) -> g{AC,#}(x13,x14) AC-DP unlabeling: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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) 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) 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() m(one(),x) -> x m(x,one()) -> x m(x,m(y,z)) -> m(m(x,y),z) m(z,pAC(x,y)) -> pAC(m(z,x),m(z,y)) m(pAC(x,y),z) -> pAC(m(x,z),m(y,z)) gAC(x,n()) -> x gAC(x,inv(x)) -> n() sm(x,sm(y,z)) -> sm(m(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(m(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(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) Usable Rule Processor: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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) 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) 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(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) AC-KBO Processor: argument filtering: pi(pAC) = [0,1] pi(zero) = [] pi(i) = 0 precedence: i > pAC > zero weight function: w0 = 2 w(zero) = 4 w(i) = w(pAC) = 0 usable rules: pAC(x,zero()) -> x pAC(i(x),x) -> zero() problem: Equations#: pAC(pAC(x3,x4),x5) -> pAC(x3,pAC(x4,x5)) pAC(x3,x4) -> pAC(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) 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) 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) 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(x12,x13),x14) -> pAC(x12,x13) pAC(x12,pAC(x13,x14)) -> pAC(x13,x14) gAC(gAC(x12,x13),x14) -> gAC(x12,x13) gAC(x12,gAC(x13,x14)) -> gAC(x13,x14) Qed