YES Time: 0.297 Problem: Equations: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) TRS: h(L(x)) -> 0() h(NAC(x,y)) -> maxAC(h(x),h(y)) maxAC(0(),x) -> x maxAC(x,0()) -> x maxAC(s(x),s(y)) -> s(maxxAC(x,y)) maxxAC(0(),x) -> x maxxAC(x,0()) -> x maxxAC(s(x),s(y)) -> s(maxAC(x,y)) Proof: DP Processor: Equations#: N{AC,#}(NAC(x3,x4),x5) -> N{AC,#}(x3,NAC(x4,x5)) N{AC,#}(x3,x4) -> N{AC,#}(x4,x3) max{AC,#}(maxAC(x3,x4),x5) -> max{AC,#}(x3,maxAC(x4,x5)) max{AC,#}(x3,x4) -> max{AC,#}(x4,x3) maxx{AC,#}(maxxAC(x3,x4),x5) -> maxx{AC,#}(x3,maxxAC(x4,x5)) maxx{AC,#}(x3,x4) -> maxx{AC,#}(x4,x3) N{AC,#}(x3,NAC(x4,x5)) -> N{AC,#}(NAC(x3,x4),x5) N{AC,#}(x4,x3) -> N{AC,#}(x3,x4) max{AC,#}(x3,maxAC(x4,x5)) -> max{AC,#}(maxAC(x3,x4),x5) max{AC,#}(x4,x3) -> max{AC,#}(x3,x4) maxx{AC,#}(x3,maxxAC(x4,x5)) -> maxx{AC,#}(maxxAC(x3,x4),x5) maxx{AC,#}(x4,x3) -> maxx{AC,#}(x3,x4) DPs: h#(NAC(x,y)) -> h#(y) h#(NAC(x,y)) -> h#(x) h#(NAC(x,y)) -> max{AC,#}(h(x),h(y)) max{AC,#}(s(x),s(y)) -> maxx{AC,#}(x,y) maxx{AC,#}(s(x),s(y)) -> max{AC,#}(x,y) max{AC,#}(x6,maxAC(0(),x)) -> max{AC,#}(x6,x) max{AC,#}(x7,maxAC(x,0())) -> max{AC,#}(x7,x) max{AC,#}(x8,maxAC(s(x),s(y))) -> maxx{AC,#}(x,y) max{AC,#}(x8,maxAC(s(x),s(y))) -> max{AC,#}(x8,s(maxxAC(x,y))) maxx{AC,#}(x9,maxxAC(0(),x)) -> maxx{AC,#}(x9,x) maxx{AC,#}(x10,maxxAC(x,0())) -> maxx{AC,#}(x10,x) maxx{AC,#}(x11,maxxAC(s(x),s(y))) -> max{AC,#}(x,y) maxx{AC,#}(x11,maxxAC(s(x),s(y))) -> maxx{AC,#}(x11,s(maxAC(x,y))) Equations: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) TRS: h(L(x)) -> 0() h(NAC(x,y)) -> maxAC(h(x),h(y)) maxAC(0(),x) -> x maxAC(x,0()) -> x maxAC(s(x),s(y)) -> s(maxxAC(x,y)) maxxAC(0(),x) -> x maxxAC(x,0()) -> x maxxAC(s(x),s(y)) -> s(maxAC(x,y)) S: N{AC,#}(NAC(x12,x13),x14) -> N{AC,#}(x12,x13) N{AC,#}(x12,NAC(x13,x14)) -> N{AC,#}(x13,x14) max{AC,#}(maxAC(x12,x13),x14) -> max{AC,#}(x12,x13) max{AC,#}(x12,maxAC(x13,x14)) -> max{AC,#}(x13,x14) maxx{AC,#}(maxxAC(x12,x13),x14) -> maxx{AC,#}(x12,x13) maxx{AC,#}(x12,maxxAC(x13,x14)) -> maxx{AC,#}(x13,x14) AC-EDG Processor: Equations#: N{AC,#}(NAC(x3,x4),x5) -> N{AC,#}(x3,NAC(x4,x5)) N{AC,#}(x3,x4) -> N{AC,#}(x4,x3) max{AC,#}(maxAC(x3,x4),x5) -> max{AC,#}(x3,maxAC(x4,x5)) max{AC,#}(x3,x4) -> max{AC,#}(x4,x3) maxx{AC,#}(maxxAC(x3,x4),x5) -> maxx{AC,#}(x3,maxxAC(x4,x5)) maxx{AC,#}(x3,x4) -> maxx{AC,#}(x4,x3) N{AC,#}(x3,NAC(x4,x5)) -> N{AC,#}(NAC(x3,x4),x5) N{AC,#}(x4,x3) -> N{AC,#}(x3,x4) max{AC,#}(x3,maxAC(x4,x5)) -> max{AC,#}(maxAC(x3,x4),x5) max{AC,#}(x4,x3) -> max{AC,#}(x3,x4) maxx{AC,#}(x3,maxxAC(x4,x5)) -> maxx{AC,#}(maxxAC(x3,x4),x5) maxx{AC,#}(x4,x3) -> maxx{AC,#}(x3,x4) DPs: h#(NAC(x,y)) -> h#(y) h#(NAC(x,y)) -> h#(x) h#(NAC(x,y)) -> max{AC,#}(h(x),h(y)) max{AC,#}(s(x),s(y)) -> maxx{AC,#}(x,y) maxx{AC,#}(s(x),s(y)) -> max{AC,#}(x,y) max{AC,#}(x6,maxAC(0(),x)) -> max{AC,#}(x6,x) max{AC,#}(x7,maxAC(x,0())) -> max{AC,#}(x7,x) max{AC,#}(x8,maxAC(s(x),s(y))) -> maxx{AC,#}(x,y) max{AC,#}(x8,maxAC(s(x),s(y))) -> max{AC,#}(x8,s(maxxAC(x,y))) maxx{AC,#}(x9,maxxAC(0(),x)) -> maxx{AC,#}(x9,x) maxx{AC,#}(x10,maxxAC(x,0())) -> maxx{AC,#}(x10,x) maxx{AC,#}(x11,maxxAC(s(x),s(y))) -> max{AC,#}(x,y) maxx{AC,#}(x11,maxxAC(s(x),s(y))) -> maxx{AC,#}(x11,s(maxAC(x,y))) Equations: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) TRS: h(L(x)) -> 0() h(NAC(x,y)) -> maxAC(h(x),h(y)) maxAC(0(),x) -> x maxAC(x,0()) -> x maxAC(s(x),s(y)) -> s(maxxAC(x,y)) maxxAC(0(),x) -> x maxxAC(x,0()) -> x maxxAC(s(x),s(y)) -> s(maxAC(x,y)) S: N{AC,#}(NAC(x12,x13),x14) -> N{AC,#}(x12,x13) N{AC,#}(x12,NAC(x13,x14)) -> N{AC,#}(x13,x14) max{AC,#}(maxAC(x12,x13),x14) -> max{AC,#}(x12,x13) max{AC,#}(x12,maxAC(x13,x14)) -> max{AC,#}(x13,x14) maxx{AC,#}(maxxAC(x12,x13),x14) -> maxx{AC,#}(x12,x13) maxx{AC,#}(x12,maxxAC(x13,x14)) -> maxx{AC,#}(x13,x14) SCC Processor: #sccs: 2 #rules: 12 #arcs: 61/169 Equations#: N{AC,#}(NAC(x3,x4),x5) -> N{AC,#}(x3,NAC(x4,x5)) N{AC,#}(x3,x4) -> N{AC,#}(x4,x3) max{AC,#}(maxAC(x3,x4),x5) -> max{AC,#}(x3,maxAC(x4,x5)) max{AC,#}(x3,x4) -> max{AC,#}(x4,x3) maxx{AC,#}(maxxAC(x3,x4),x5) -> maxx{AC,#}(x3,maxxAC(x4,x5)) maxx{AC,#}(x3,x4) -> maxx{AC,#}(x4,x3) N{AC,#}(x3,NAC(x4,x5)) -> N{AC,#}(NAC(x3,x4),x5) N{AC,#}(x4,x3) -> N{AC,#}(x3,x4) max{AC,#}(x3,maxAC(x4,x5)) -> max{AC,#}(maxAC(x3,x4),x5) max{AC,#}(x4,x3) -> max{AC,#}(x3,x4) maxx{AC,#}(x3,maxxAC(x4,x5)) -> maxx{AC,#}(maxxAC(x3,x4),x5) maxx{AC,#}(x4,x3) -> maxx{AC,#}(x3,x4) DPs: h#(NAC(x,y)) -> h#(y) h#(NAC(x,y)) -> h#(x) Equations: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) TRS: h(L(x)) -> 0() h(NAC(x,y)) -> maxAC(h(x),h(y)) maxAC(0(),x) -> x maxAC(x,0()) -> x maxAC(s(x),s(y)) -> s(maxxAC(x,y)) maxxAC(0(),x) -> x maxxAC(x,0()) -> x maxxAC(s(x),s(y)) -> s(maxAC(x,y)) S: N{AC,#}(NAC(x12,x13),x14) -> N{AC,#}(x12,x13) N{AC,#}(x12,NAC(x13,x14)) -> N{AC,#}(x13,x14) max{AC,#}(maxAC(x12,x13),x14) -> max{AC,#}(x12,x13) max{AC,#}(x12,maxAC(x13,x14)) -> max{AC,#}(x13,x14) maxx{AC,#}(maxxAC(x12,x13),x14) -> maxx{AC,#}(x12,x13) maxx{AC,#}(x12,maxxAC(x13,x14)) -> maxx{AC,#}(x13,x14) AC-DP unlabeling: Equations#: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) DPs: h#(NAC(x,y)) -> h#(y) h#(NAC(x,y)) -> h#(x) Equations: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) TRS: h(L(x)) -> 0() h(NAC(x,y)) -> maxAC(h(x),h(y)) maxAC(0(),x) -> x maxAC(x,0()) -> x maxAC(s(x),s(y)) -> s(maxxAC(x,y)) maxxAC(0(),x) -> x maxxAC(x,0()) -> x maxxAC(s(x),s(y)) -> s(maxAC(x,y)) S: NAC(NAC(x12,x13),x14) -> NAC(x12,x13) NAC(x12,NAC(x13,x14)) -> NAC(x13,x14) maxAC(maxAC(x12,x13),x14) -> maxAC(x12,x13) maxAC(x12,maxAC(x13,x14)) -> maxAC(x13,x14) maxxAC(maxxAC(x12,x13),x14) -> maxxAC(x12,x13) maxxAC(x12,maxxAC(x13,x14)) -> maxxAC(x13,x14) Usable Rule Processor: Equations#: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) DPs: h#(NAC(x,y)) -> h#(y) h#(NAC(x,y)) -> h#(x) Equations: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) TRS: S: NAC(NAC(x12,x13),x14) -> NAC(x12,x13) NAC(x12,NAC(x13,x14)) -> NAC(x13,x14) maxAC(maxAC(x12,x13),x14) -> maxAC(x12,x13) maxAC(x12,maxAC(x13,x14)) -> maxAC(x13,x14) maxxAC(maxxAC(x12,x13),x14) -> maxxAC(x12,x13) maxxAC(x12,maxxAC(x13,x14)) -> maxxAC(x13,x14) AC-KBO Processor: argument filtering: pi(NAC) = [0,1] pi(h#) = [0] precedence: h# > NAC weight function: [h#](x0) = 4x0 + 4, [NAC](x0, x1) = x0 + x1 usable rules: problem: Equations#: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) DPs: Equations: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) TRS: S: NAC(NAC(x12,x13),x14) -> NAC(x12,x13) NAC(x12,NAC(x13,x14)) -> NAC(x13,x14) maxAC(maxAC(x12,x13),x14) -> maxAC(x12,x13) maxAC(x12,maxAC(x13,x14)) -> maxAC(x13,x14) maxxAC(maxxAC(x12,x13),x14) -> maxxAC(x12,x13) maxxAC(x12,maxxAC(x13,x14)) -> maxxAC(x13,x14) Qed Equations#: N{AC,#}(NAC(x3,x4),x5) -> N{AC,#}(x3,NAC(x4,x5)) N{AC,#}(x3,x4) -> N{AC,#}(x4,x3) max{AC,#}(maxAC(x3,x4),x5) -> max{AC,#}(x3,maxAC(x4,x5)) max{AC,#}(x3,x4) -> max{AC,#}(x4,x3) maxx{AC,#}(maxxAC(x3,x4),x5) -> maxx{AC,#}(x3,maxxAC(x4,x5)) maxx{AC,#}(x3,x4) -> maxx{AC,#}(x4,x3) N{AC,#}(x3,NAC(x4,x5)) -> N{AC,#}(NAC(x3,x4),x5) N{AC,#}(x4,x3) -> N{AC,#}(x3,x4) max{AC,#}(x3,maxAC(x4,x5)) -> max{AC,#}(maxAC(x3,x4),x5) max{AC,#}(x4,x3) -> max{AC,#}(x3,x4) maxx{AC,#}(x3,maxxAC(x4,x5)) -> maxx{AC,#}(maxxAC(x3,x4),x5) maxx{AC,#}(x4,x3) -> maxx{AC,#}(x3,x4) DPs: maxx{AC,#}(s(x),s(y)) -> max{AC,#}(x,y) max{AC,#}(x8,maxAC(s(x),s(y))) -> max{AC,#}(x8,s(maxxAC(x,y))) max{AC,#}(x8,maxAC(s(x),s(y))) -> maxx{AC,#}(x,y) maxx{AC,#}(x11,maxxAC(s(x),s(y))) -> maxx{AC,#}(x11,s(maxAC(x,y))) maxx{AC,#}(x11,maxxAC(s(x),s(y))) -> max{AC,#}(x,y) max{AC,#}(x7,maxAC(x,0())) -> max{AC,#}(x7,x) max{AC,#}(x6,maxAC(0(),x)) -> max{AC,#}(x6,x) max{AC,#}(s(x),s(y)) -> maxx{AC,#}(x,y) maxx{AC,#}(x10,maxxAC(x,0())) -> maxx{AC,#}(x10,x) maxx{AC,#}(x9,maxxAC(0(),x)) -> maxx{AC,#}(x9,x) Equations: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) TRS: h(L(x)) -> 0() h(NAC(x,y)) -> maxAC(h(x),h(y)) maxAC(0(),x) -> x maxAC(x,0()) -> x maxAC(s(x),s(y)) -> s(maxxAC(x,y)) maxxAC(0(),x) -> x maxxAC(x,0()) -> x maxxAC(s(x),s(y)) -> s(maxAC(x,y)) S: N{AC,#}(NAC(x12,x13),x14) -> N{AC,#}(x12,x13) N{AC,#}(x12,NAC(x13,x14)) -> N{AC,#}(x13,x14) max{AC,#}(maxAC(x12,x13),x14) -> max{AC,#}(x12,x13) max{AC,#}(x12,maxAC(x13,x14)) -> max{AC,#}(x13,x14) maxx{AC,#}(maxxAC(x12,x13),x14) -> maxx{AC,#}(x12,x13) maxx{AC,#}(x12,maxxAC(x13,x14)) -> maxx{AC,#}(x13,x14) AC-DP unlabeling: Equations#: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) DPs: maxxAC(s(x),s(y)) -> maxAC(x,y) maxAC(x8,maxAC(s(x),s(y))) -> maxAC(x8,s(maxxAC(x,y))) maxAC(x8,maxAC(s(x),s(y))) -> maxxAC(x,y) maxxAC(x11,maxxAC(s(x),s(y))) -> maxxAC(x11,s(maxAC(x,y))) maxxAC(x11,maxxAC(s(x),s(y))) -> maxAC(x,y) maxAC(x7,maxAC(x,0())) -> maxAC(x7,x) maxAC(x6,maxAC(0(),x)) -> maxAC(x6,x) maxAC(s(x),s(y)) -> maxxAC(x,y) maxxAC(x10,maxxAC(x,0())) -> maxxAC(x10,x) maxxAC(x9,maxxAC(0(),x)) -> maxxAC(x9,x) Equations: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) TRS: h(L(x)) -> 0() h(NAC(x,y)) -> maxAC(h(x),h(y)) maxAC(0(),x) -> x maxAC(x,0()) -> x maxAC(s(x),s(y)) -> s(maxxAC(x,y)) maxxAC(0(),x) -> x maxxAC(x,0()) -> x maxxAC(s(x),s(y)) -> s(maxAC(x,y)) S: NAC(NAC(x12,x13),x14) -> NAC(x12,x13) NAC(x12,NAC(x13,x14)) -> NAC(x13,x14) maxAC(maxAC(x12,x13),x14) -> maxAC(x12,x13) maxAC(x12,maxAC(x13,x14)) -> maxAC(x13,x14) maxxAC(maxxAC(x12,x13),x14) -> maxxAC(x12,x13) maxxAC(x12,maxxAC(x13,x14)) -> maxxAC(x13,x14) Usable Rule Processor: Equations#: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) DPs: maxxAC(s(x),s(y)) -> maxAC(x,y) maxAC(x8,maxAC(s(x),s(y))) -> maxAC(x8,s(maxxAC(x,y))) maxAC(x8,maxAC(s(x),s(y))) -> maxxAC(x,y) maxxAC(x11,maxxAC(s(x),s(y))) -> maxxAC(x11,s(maxAC(x,y))) maxxAC(x11,maxxAC(s(x),s(y))) -> maxAC(x,y) maxAC(x7,maxAC(x,0())) -> maxAC(x7,x) maxAC(x6,maxAC(0(),x)) -> maxAC(x6,x) maxAC(s(x),s(y)) -> maxxAC(x,y) maxxAC(x10,maxxAC(x,0())) -> maxxAC(x10,x) maxxAC(x9,maxxAC(0(),x)) -> maxxAC(x9,x) Equations: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) TRS: maxAC(0(),x) -> x maxAC(x,0()) -> x maxAC(s(x),s(y)) -> s(maxxAC(x,y)) maxxAC(0(),x) -> x maxxAC(x,0()) -> x maxxAC(s(x),s(y)) -> s(maxAC(x,y)) S: NAC(NAC(x12,x13),x14) -> NAC(x12,x13) NAC(x12,NAC(x13,x14)) -> NAC(x13,x14) maxAC(maxAC(x12,x13),x14) -> maxAC(x12,x13) maxAC(x12,maxAC(x13,x14)) -> maxAC(x13,x14) maxxAC(maxxAC(x12,x13),x14) -> maxxAC(x12,x13) maxxAC(x12,maxxAC(x13,x14)) -> maxxAC(x13,x14) AC-KBO Processor: argument filtering: pi(maxAC) = [0,1] pi(maxxAC) = [0,1] pi(0) = [] pi(s) = [0] precedence: s > 0 ~ maxxAC ~ maxAC weight function: [s](x0) = x0 + 1, [0] = 4, [maxxAC](x0, x1) = x0 + x1 + 6, [maxAC](x0, x1) = x0 + x1 + 6 usable rules: maxAC(0(),x) -> x maxAC(x,0()) -> x maxAC(s(x),s(y)) -> s(maxxAC(x,y)) maxxAC(0(),x) -> x maxxAC(x,0()) -> x maxxAC(s(x),s(y)) -> s(maxAC(x,y)) problem: Equations#: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) DPs: Equations: NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5)) NAC(x3,x4) -> NAC(x4,x3) maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5)) maxAC(x3,x4) -> maxAC(x4,x3) maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5)) maxxAC(x3,x4) -> maxxAC(x4,x3) NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5) NAC(x4,x3) -> NAC(x3,x4) maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5) maxAC(x4,x3) -> maxAC(x3,x4) maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5) maxxAC(x4,x3) -> maxxAC(x3,x4) TRS: maxAC(0(),x) -> x maxAC(x,0()) -> x maxAC(s(x),s(y)) -> s(maxxAC(x,y)) maxxAC(0(),x) -> x maxxAC(x,0()) -> x maxxAC(s(x),s(y)) -> s(maxAC(x,y)) S: NAC(NAC(x12,x13),x14) -> NAC(x12,x13) NAC(x12,NAC(x13,x14)) -> NAC(x13,x14) maxAC(maxAC(x12,x13),x14) -> maxAC(x12,x13) maxAC(x12,maxAC(x13,x14)) -> maxAC(x13,x14) maxxAC(maxxAC(x12,x13),x14) -> maxxAC(x12,x13) maxxAC(x12,maxxAC(x13,x14)) -> maxxAC(x13,x14) Qed