YES Time: 0.217 Problem: Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) Proof: DP Processor: Equations#: min{AC,#}(minAC(x3,x4),x5) -> min{AC,#}(x3,minAC(x4,x5)) min{AC,#}(x3,x4) -> min{AC,#}(x4,x3) max{AC,#}(maxAC(x3,x4),x5) -> max{AC,#}(x3,maxAC(x4,x5)) max{AC,#}(x3,x4) -> max{AC,#}(x4,x3) min{AC,#}(x3,minAC(x4,x5)) -> min{AC,#}(minAC(x3,x4),x5) min{AC,#}(x4,x3) -> min{AC,#}(x3,x4) max{AC,#}(x3,maxAC(x4,x5)) -> max{AC,#}(maxAC(x3,x4),x5) max{AC,#}(x4,x3) -> max{AC,#}(x3,x4) DPs: plus#(x,s(y)) -> plus#(x,y) min{AC,#}(s(x),s(y)) -> min{AC,#}(x,y) max{AC,#}(s(x),s(y)) -> max{AC,#}(x,y) min{AC,#}(x6,minAC(0(),y)) -> min{AC,#}(x6,0()) min{AC,#}(x7,minAC(s(x),s(y))) -> min{AC,#}(x,y) min{AC,#}(x7,minAC(s(x),s(y))) -> min{AC,#}(x7,s(minAC(x,y))) max{AC,#}(x8,maxAC(0(),y)) -> max{AC,#}(x8,y) max{AC,#}(x9,maxAC(s(x),s(y))) -> max{AC,#}(x,y) max{AC,#}(x9,maxAC(s(x),s(y))) -> max{AC,#}(x9,s(maxAC(x,y))) Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) S: min{AC,#}(minAC(x10,x11),x12) -> min{AC,#}(x10,x11) min{AC,#}(x10,minAC(x11,x12)) -> min{AC,#}(x11,x12) max{AC,#}(maxAC(x10,x11),x12) -> max{AC,#}(x10,x11) max{AC,#}(x10,maxAC(x11,x12)) -> max{AC,#}(x11,x12) AC-EDG Processor: Equations#: min{AC,#}(minAC(x3,x4),x5) -> min{AC,#}(x3,minAC(x4,x5)) min{AC,#}(x3,x4) -> min{AC,#}(x4,x3) max{AC,#}(maxAC(x3,x4),x5) -> max{AC,#}(x3,maxAC(x4,x5)) max{AC,#}(x3,x4) -> max{AC,#}(x4,x3) min{AC,#}(x3,minAC(x4,x5)) -> min{AC,#}(minAC(x3,x4),x5) min{AC,#}(x4,x3) -> min{AC,#}(x3,x4) max{AC,#}(x3,maxAC(x4,x5)) -> max{AC,#}(maxAC(x3,x4),x5) max{AC,#}(x4,x3) -> max{AC,#}(x3,x4) DPs: plus#(x,s(y)) -> plus#(x,y) min{AC,#}(s(x),s(y)) -> min{AC,#}(x,y) max{AC,#}(s(x),s(y)) -> max{AC,#}(x,y) min{AC,#}(x6,minAC(0(),y)) -> min{AC,#}(x6,0()) min{AC,#}(x7,minAC(s(x),s(y))) -> min{AC,#}(x,y) min{AC,#}(x7,minAC(s(x),s(y))) -> min{AC,#}(x7,s(minAC(x,y))) max{AC,#}(x8,maxAC(0(),y)) -> max{AC,#}(x8,y) max{AC,#}(x9,maxAC(s(x),s(y))) -> max{AC,#}(x,y) max{AC,#}(x9,maxAC(s(x),s(y))) -> max{AC,#}(x9,s(maxAC(x,y))) Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) S: min{AC,#}(minAC(x10,x11),x12) -> min{AC,#}(x10,x11) min{AC,#}(x10,minAC(x11,x12)) -> min{AC,#}(x11,x12) max{AC,#}(maxAC(x10,x11),x12) -> max{AC,#}(x10,x11) max{AC,#}(x10,maxAC(x11,x12)) -> max{AC,#}(x11,x12) SCC Processor: #sccs: 3 #rules: 9 #arcs: 33/81 Equations#: min{AC,#}(minAC(x3,x4),x5) -> min{AC,#}(x3,minAC(x4,x5)) min{AC,#}(x3,x4) -> min{AC,#}(x4,x3) max{AC,#}(maxAC(x3,x4),x5) -> max{AC,#}(x3,maxAC(x4,x5)) max{AC,#}(x3,x4) -> max{AC,#}(x4,x3) min{AC,#}(x3,minAC(x4,x5)) -> min{AC,#}(minAC(x3,x4),x5) min{AC,#}(x4,x3) -> min{AC,#}(x3,x4) max{AC,#}(x3,maxAC(x4,x5)) -> max{AC,#}(maxAC(x3,x4),x5) max{AC,#}(x4,x3) -> max{AC,#}(x3,x4) DPs: plus#(x,s(y)) -> plus#(x,y) Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) S: min{AC,#}(minAC(x10,x11),x12) -> min{AC,#}(x10,x11) min{AC,#}(x10,minAC(x11,x12)) -> min{AC,#}(x11,x12) max{AC,#}(maxAC(x10,x11),x12) -> max{AC,#}(x10,x11) max{AC,#}(x10,maxAC(x11,x12)) -> max{AC,#}(x11,x12) AC-DP unlabeling: Equations#: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) DPs: plus#(x,s(y)) -> plus#(x,y) Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) S: minAC(minAC(x10,x11),x12) -> minAC(x10,x11) minAC(x10,minAC(x11,x12)) -> minAC(x11,x12) maxAC(maxAC(x10,x11),x12) -> maxAC(x10,x11) maxAC(x10,maxAC(x11,x12)) -> maxAC(x11,x12) Usable Rule Processor: Equations#: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) DPs: plus#(x,s(y)) -> plus#(x,y) Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: S: minAC(minAC(x10,x11),x12) -> minAC(x10,x11) minAC(x10,minAC(x11,x12)) -> minAC(x11,x12) maxAC(maxAC(x10,x11),x12) -> maxAC(x10,x11) maxAC(x10,maxAC(x11,x12)) -> maxAC(x11,x12) AC-KBO Processor: argument filtering: pi(s) = [0] pi(plus#) = 1 precedence: plus# ~ s weight function: w0 = 2 w(plus#) = 2 w(s) = 0 usable rules: problem: Equations#: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) DPs: Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: S: minAC(minAC(x10,x11),x12) -> minAC(x10,x11) minAC(x10,minAC(x11,x12)) -> minAC(x11,x12) maxAC(maxAC(x10,x11),x12) -> maxAC(x10,x11) maxAC(x10,maxAC(x11,x12)) -> maxAC(x11,x12) Qed Equations#: min{AC,#}(minAC(x3,x4),x5) -> min{AC,#}(x3,minAC(x4,x5)) min{AC,#}(x3,x4) -> min{AC,#}(x4,x3) max{AC,#}(maxAC(x3,x4),x5) -> max{AC,#}(x3,maxAC(x4,x5)) max{AC,#}(x3,x4) -> max{AC,#}(x4,x3) min{AC,#}(x3,minAC(x4,x5)) -> min{AC,#}(minAC(x3,x4),x5) min{AC,#}(x4,x3) -> min{AC,#}(x3,x4) max{AC,#}(x3,maxAC(x4,x5)) -> max{AC,#}(maxAC(x3,x4),x5) max{AC,#}(x4,x3) -> max{AC,#}(x3,x4) DPs: min{AC,#}(s(x),s(y)) -> min{AC,#}(x,y) min{AC,#}(x7,minAC(s(x),s(y))) -> min{AC,#}(x7,s(minAC(x,y))) min{AC,#}(x7,minAC(s(x),s(y))) -> min{AC,#}(x,y) min{AC,#}(x6,minAC(0(),y)) -> min{AC,#}(x6,0()) Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) S: min{AC,#}(minAC(x10,x11),x12) -> min{AC,#}(x10,x11) min{AC,#}(x10,minAC(x11,x12)) -> min{AC,#}(x11,x12) max{AC,#}(maxAC(x10,x11),x12) -> max{AC,#}(x10,x11) max{AC,#}(x10,maxAC(x11,x12)) -> max{AC,#}(x11,x12) AC-DP unlabeling: Equations#: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) DPs: minAC(s(x),s(y)) -> minAC(x,y) minAC(x7,minAC(s(x),s(y))) -> minAC(x7,s(minAC(x,y))) minAC(x7,minAC(s(x),s(y))) -> minAC(x,y) minAC(x6,minAC(0(),y)) -> minAC(x6,0()) Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) S: minAC(minAC(x10,x11),x12) -> minAC(x10,x11) minAC(x10,minAC(x11,x12)) -> minAC(x11,x12) maxAC(maxAC(x10,x11),x12) -> maxAC(x10,x11) maxAC(x10,maxAC(x11,x12)) -> maxAC(x11,x12) Usable Rule Processor: Equations#: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) DPs: minAC(s(x),s(y)) -> minAC(x,y) minAC(x7,minAC(s(x),s(y))) -> minAC(x7,s(minAC(x,y))) minAC(x7,minAC(s(x),s(y))) -> minAC(x,y) minAC(x6,minAC(0(),y)) -> minAC(x6,0()) Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) S: minAC(minAC(x10,x11),x12) -> minAC(x10,x11) minAC(x10,minAC(x11,x12)) -> minAC(x11,x12) maxAC(maxAC(x10,x11),x12) -> maxAC(x10,x11) maxAC(x10,maxAC(x11,x12)) -> maxAC(x11,x12) AC-KBO Processor: argument filtering: pi(minAC) = [0,1] pi(0) = [] pi(s) = [0] precedence: 0 ~ minAC > s weight function: w0 = 1 w(minAC) = 5 w(0) = 4 w(s) = 2 usable rules: minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) problem: Equations#: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) DPs: Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) S: minAC(minAC(x10,x11),x12) -> minAC(x10,x11) minAC(x10,minAC(x11,x12)) -> minAC(x11,x12) maxAC(maxAC(x10,x11),x12) -> maxAC(x10,x11) maxAC(x10,maxAC(x11,x12)) -> maxAC(x11,x12) Qed Equations#: min{AC,#}(minAC(x3,x4),x5) -> min{AC,#}(x3,minAC(x4,x5)) min{AC,#}(x3,x4) -> min{AC,#}(x4,x3) max{AC,#}(maxAC(x3,x4),x5) -> max{AC,#}(x3,maxAC(x4,x5)) max{AC,#}(x3,x4) -> max{AC,#}(x4,x3) min{AC,#}(x3,minAC(x4,x5)) -> min{AC,#}(minAC(x3,x4),x5) min{AC,#}(x4,x3) -> min{AC,#}(x3,x4) max{AC,#}(x3,maxAC(x4,x5)) -> max{AC,#}(maxAC(x3,x4),x5) max{AC,#}(x4,x3) -> max{AC,#}(x3,x4) DPs: max{AC,#}(s(x),s(y)) -> max{AC,#}(x,y) max{AC,#}(x9,maxAC(s(x),s(y))) -> max{AC,#}(x9,s(maxAC(x,y))) max{AC,#}(x9,maxAC(s(x),s(y))) -> max{AC,#}(x,y) max{AC,#}(x8,maxAC(0(),y)) -> max{AC,#}(x8,y) Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) S: min{AC,#}(minAC(x10,x11),x12) -> min{AC,#}(x10,x11) min{AC,#}(x10,minAC(x11,x12)) -> min{AC,#}(x11,x12) max{AC,#}(maxAC(x10,x11),x12) -> max{AC,#}(x10,x11) max{AC,#}(x10,maxAC(x11,x12)) -> max{AC,#}(x11,x12) AC-DP unlabeling: Equations#: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) DPs: maxAC(s(x),s(y)) -> maxAC(x,y) maxAC(x9,maxAC(s(x),s(y))) -> maxAC(x9,s(maxAC(x,y))) maxAC(x9,maxAC(s(x),s(y))) -> maxAC(x,y) maxAC(x8,maxAC(0(),y)) -> maxAC(x8,y) Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: plus(x,0()) -> x plus(x,s(y)) -> s(plus(x,y)) minAC(0(),y) -> 0() minAC(s(x),s(y)) -> s(minAC(x,y)) maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) S: minAC(minAC(x10,x11),x12) -> minAC(x10,x11) minAC(x10,minAC(x11,x12)) -> minAC(x11,x12) maxAC(maxAC(x10,x11),x12) -> maxAC(x10,x11) maxAC(x10,maxAC(x11,x12)) -> maxAC(x11,x12) Usable Rule Processor: Equations#: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) DPs: maxAC(s(x),s(y)) -> maxAC(x,y) maxAC(x9,maxAC(s(x),s(y))) -> maxAC(x9,s(maxAC(x,y))) maxAC(x9,maxAC(s(x),s(y))) -> maxAC(x,y) maxAC(x8,maxAC(0(),y)) -> maxAC(x8,y) Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) S: minAC(minAC(x10,x11),x12) -> minAC(x10,x11) minAC(x10,minAC(x11,x12)) -> minAC(x11,x12) maxAC(maxAC(x10,x11),x12) -> maxAC(x10,x11) maxAC(x10,maxAC(x11,x12)) -> maxAC(x11,x12) AC-KBO Processor: argument filtering: pi(maxAC) = [0,1] pi(0) = [] pi(s) = [0] precedence: 0 ~ maxAC > s weight function: w0 = 1 w(s) = 4 w(0) = 2 w(maxAC) = 1 usable rules: maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) problem: Equations#: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) DPs: Equations: minAC(minAC(x3,x4),x5) -> minAC(x3,minAC(x4,x5)) minAC(x3,x4) -> minAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) minAC(x3,minAC(x4,x5)) -> minAC(minAC(x3,x4),x5) minAC(x4,x3) -> minAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) TRS: maxAC(0(),y) -> y maxAC(s(x),s(y)) -> s(maxAC(x,y)) S: minAC(minAC(x10,x11),x12) -> minAC(x10,x11) minAC(x10,minAC(x11,x12)) -> minAC(x11,x12) maxAC(maxAC(x10,x11),x12) -> maxAC(x10,x11) maxAC(x10,maxAC(x11,x12)) -> maxAC(x11,x12) Qed