YES Problem: ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) -> ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) -> choice(S,cons(u,K),E) choice(cons(u,S),K,E) -> choice(S,K,E) Proof: DP Processor: DPs: find#(u,v,cons(cons(u2,v2),E)) -> find#(u,v,E) complete#(u,cons(v,S),E) -> complete#(u,S,E) complete#(u,cons(v,S),E) -> find#(u,v,E) complete#(u,cons(v,S),E) -> ite#(find(u,v,E),complete(u,S,E),ff()) clique#(cons(u,K),E) -> clique#(K,E) clique#(cons(u,K),E) -> complete#(u,K,E) clique#(cons(u,K),E) -> ite#(complete(u,K,E),clique(K,E),ff()) choice#(nil(),K,E) -> clique#(K,E) choice#(nil(),K,E) -> ite#(clique(K,E),K,nil()) choice#(cons(u,S),K,E) -> choice#(S,cons(u,K),E) choice#(cons(u,S),K,E) -> choice#(S,K,E) TRS: ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) -> ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) -> choice(S,cons(u,K),E) choice(cons(u,S),K,E) -> choice(S,K,E) Usable Rule Processor: DPs: find#(u,v,cons(cons(u2,v2),E)) -> find#(u,v,E) complete#(u,cons(v,S),E) -> complete#(u,S,E) complete#(u,cons(v,S),E) -> find#(u,v,E) complete#(u,cons(v,S),E) -> ite#(find(u,v,E),complete(u,S,E),ff()) clique#(cons(u,K),E) -> clique#(K,E) clique#(cons(u,K),E) -> complete#(u,K,E) clique#(cons(u,K),E) -> ite#(complete(u,K,E),clique(K,E),ff()) choice#(nil(),K,E) -> clique#(K,E) choice#(nil(),K,E) -> ite#(clique(K,E),K,nil()) choice#(cons(u,S),K,E) -> choice#(S,cons(u,K),E) choice#(cons(u,S),K,E) -> choice#(S,K,E) TRS: f14(x,y) -> x f14(x,y) -> y complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) ADG Processor: DPs: find#(u,v,cons(cons(u2,v2),E)) -> find#(u,v,E) complete#(u,cons(v,S),E) -> complete#(u,S,E) complete#(u,cons(v,S),E) -> find#(u,v,E) complete#(u,cons(v,S),E) -> ite#(find(u,v,E),complete(u,S,E),ff()) clique#(cons(u,K),E) -> clique#(K,E) clique#(cons(u,K),E) -> complete#(u,K,E) clique#(cons(u,K),E) -> ite#(complete(u,K,E),clique(K,E),ff()) choice#(nil(),K,E) -> clique#(K,E) choice#(nil(),K,E) -> ite#(clique(K,E),K,nil()) choice#(cons(u,S),K,E) -> choice#(S,cons(u,K),E) choice#(cons(u,S),K,E) -> choice#(S,K,E) TRS: f14(x,y) -> x f14(x,y) -> y complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) graph: choice#(cons(u,S),K,E) -> choice#(S,cons(u,K),E) -> choice#(nil(),K,E) -> clique#(K,E) choice#(cons(u,S),K,E) -> choice#(S,cons(u,K),E) -> choice#(nil(),K,E) -> ite#(clique(K,E),K,nil()) choice#(cons(u,S),K,E) -> choice#(S,cons(u,K),E) -> choice#(cons(u,S),K,E) -> choice#(S,cons(u,K),E) choice#(cons(u,S),K,E) -> choice#(S,cons(u,K),E) -> choice#(cons(u,S),K,E) -> choice#(S,K,E) choice#(cons(u,S),K,E) -> choice#(S,K,E) -> choice#(nil(),K,E) -> clique#(K,E) choice#(cons(u,S),K,E) -> choice#(S,K,E) -> choice#(nil(),K,E) -> ite#(clique(K,E),K,nil()) choice#(cons(u,S),K,E) -> choice#(S,K,E) -> choice#(cons(u,S),K,E) -> choice#(S,cons(u,K),E) choice#(cons(u,S),K,E) -> choice#(S,K,E) -> choice#(cons(u,S),K,E) -> choice#(S,K,E) choice#(nil(),K,E) -> clique#(K,E) -> clique#(cons(u,K),E) -> clique#(K,E) choice#(nil(),K,E) -> clique#(K,E) -> clique#(cons(u,K),E) -> complete#(u,K,E) choice#(nil(),K,E) -> clique#(K,E) -> clique#(cons(u,K),E) -> ite#(complete(u,K,E),clique(K,E),ff()) clique#(cons(u,K),E) -> clique#(K,E) -> clique#(cons(u,K),E) -> clique#(K,E) clique#(cons(u,K),E) -> clique#(K,E) -> clique#(cons(u,K),E) -> complete#(u,K,E) clique#(cons(u,K),E) -> clique#(K,E) -> clique#(cons(u,K),E) -> ite#(complete(u,K,E),clique(K,E),ff()) clique#(cons(u,K),E) -> complete#(u,K,E) -> complete#(u,cons(v,S),E) -> complete#(u,S,E) clique#(cons(u,K),E) -> complete#(u,K,E) -> complete#(u,cons(v,S),E) -> find#(u,v,E) clique#(cons(u,K),E) -> complete#(u,K,E) -> complete#(u,cons(v,S),E) -> ite#(find(u,v,E),complete(u,S,E),ff()) complete#(u,cons(v,S),E) -> complete#(u,S,E) -> complete#(u,cons(v,S),E) -> complete#(u,S,E) complete#(u,cons(v,S),E) -> complete#(u,S,E) -> complete#(u,cons(v,S),E) -> find#(u,v,E) complete#(u,cons(v,S),E) -> complete#(u,S,E) -> complete#(u,cons(v,S),E) -> ite#(find(u,v,E),complete(u,S,E),ff()) complete#(u,cons(v,S),E) -> find#(u,v,E) -> find#(u,v,cons(cons(u2,v2),E)) -> find#(u,v,E) find#(u,v,cons(cons(u2,v2),E)) -> find#(u,v,E) -> find#(u,v,cons(cons(u2,v2),E)) -> find#(u,v,E) Restore Modifier: DPs: find#(u,v,cons(cons(u2,v2),E)) -> find#(u,v,E) complete#(u,cons(v,S),E) -> complete#(u,S,E) complete#(u,cons(v,S),E) -> find#(u,v,E) complete#(u,cons(v,S),E) -> ite#(find(u,v,E),complete(u,S,E),ff()) clique#(cons(u,K),E) -> clique#(K,E) clique#(cons(u,K),E) -> complete#(u,K,E) clique#(cons(u,K),E) -> ite#(complete(u,K,E),clique(K,E),ff()) choice#(nil(),K,E) -> clique#(K,E) choice#(nil(),K,E) -> ite#(clique(K,E),K,nil()) choice#(cons(u,S),K,E) -> choice#(S,cons(u,K),E) choice#(cons(u,S),K,E) -> choice#(S,K,E) TRS: ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) -> ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) -> choice(S,cons(u,K),E) choice(cons(u,S),K,E) -> choice(S,K,E) SCC Processor: #sccs: 4 #rules: 5 #arcs: 22/121 DPs: choice#(cons(u,S),K,E) -> choice#(S,cons(u,K),E) choice#(cons(u,S),K,E) -> choice#(S,K,E) TRS: ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) -> ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) -> choice(S,cons(u,K),E) choice(cons(u,S),K,E) -> choice(S,K,E) Matrix Interpretation Processor: dimension: 1 interpretation: [choice#](x0, x1, x2) = x0 + x1 + 1, [choice](x0, x1, x2) = x0 + x1, [clique](x0, x1) = 1, [complete](x0, x1, x2) = 1, [cons](x0, x1) = x1 + 1, [find](x0, x1, x2) = x2, [nil] = 0, [ff] = 0, [ite](x0, x1, x2) = x1 + x2, [tt] = 1 orientation: choice#(cons(u,S),K,E) = K + S + 2 >= K + S + 2 = choice#(S,cons(u,K),E) choice#(cons(u,S),K,E) = K + S + 2 >= K + S + 1 = choice#(S,K,E) ite(tt(),u,v) = u + v >= u = u ite(ff(),u,v) = u + v >= v = v find(u,v,nil()) = 0 >= 0 = ff() find(u,v,cons(cons(u,v),E)) = E + 1 >= 1 = tt() find(u,v,cons(cons(u2,v2),E)) = E + 1 >= E = find(u,v,E) complete(u,nil(),E) = 1 >= 1 = tt() complete(u,cons(v,S),E) = 1 >= 1 = ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) = 1 >= 1 = tt() clique(cons(u,K),E) = 1 >= 1 = ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) = K >= K = ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) = K + S + 1 >= K + S + 1 = choice(S,cons(u,K),E) choice(cons(u,S),K,E) = K + S + 1 >= K + S = choice(S,K,E) problem: DPs: choice#(cons(u,S),K,E) -> choice#(S,cons(u,K),E) TRS: ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) -> ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) -> choice(S,cons(u,K),E) choice(cons(u,S),K,E) -> choice(S,K,E) Matrix Interpretation Processor: dimension: 1 interpretation: [choice#](x0, x1, x2) = x0, [choice](x0, x1, x2) = x0 + x1, [clique](x0, x1) = 0, [complete](x0, x1, x2) = 0, [cons](x0, x1) = x1 + 1, [find](x0, x1, x2) = 0, [nil] = 0, [ff] = 0, [ite](x0, x1, x2) = x1 + x2, [tt] = 0 orientation: choice#(cons(u,S),K,E) = S + 1 >= S = choice#(S,cons(u,K),E) ite(tt(),u,v) = u + v >= u = u ite(ff(),u,v) = u + v >= v = v find(u,v,nil()) = 0 >= 0 = ff() find(u,v,cons(cons(u,v),E)) = 0 >= 0 = tt() find(u,v,cons(cons(u2,v2),E)) = 0 >= 0 = find(u,v,E) complete(u,nil(),E) = 0 >= 0 = tt() complete(u,cons(v,S),E) = 0 >= 0 = ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) = 0 >= 0 = tt() clique(cons(u,K),E) = 0 >= 0 = ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) = K >= K = ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) = K + S + 1 >= K + S + 1 = choice(S,cons(u,K),E) choice(cons(u,S),K,E) = K + S + 1 >= K + S = choice(S,K,E) problem: DPs: TRS: ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) -> ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) -> choice(S,cons(u,K),E) choice(cons(u,S),K,E) -> choice(S,K,E) Qed DPs: clique#(cons(u,K),E) -> clique#(K,E) TRS: ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) -> ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) -> choice(S,cons(u,K),E) choice(cons(u,S),K,E) -> choice(S,K,E) Matrix Interpretation Processor: dimension: 1 interpretation: [clique#](x0, x1) = x0 + 1, [choice](x0, x1, x2) = x0 + x1, [clique](x0, x1) = 0, [complete](x0, x1, x2) = x2, [cons](x0, x1) = x0 + x1 + 1, [find](x0, x1, x2) = 0, [nil] = 0, [ff] = 0, [ite](x0, x1, x2) = x1 + x2, [tt] = 0 orientation: clique#(cons(u,K),E) = K + u + 2 >= K + 1 = clique#(K,E) ite(tt(),u,v) = u + v >= u = u ite(ff(),u,v) = u + v >= v = v find(u,v,nil()) = 0 >= 0 = ff() find(u,v,cons(cons(u,v),E)) = 0 >= 0 = tt() find(u,v,cons(cons(u2,v2),E)) = 0 >= 0 = find(u,v,E) complete(u,nil(),E) = E >= 0 = tt() complete(u,cons(v,S),E) = E >= E = ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) = 0 >= 0 = tt() clique(cons(u,K),E) = 0 >= 0 = ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) = K >= K = ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) = K + S + u + 1 >= K + S + u + 1 = choice(S,cons(u,K),E) choice(cons(u,S),K,E) = K + S + u + 1 >= K + S = choice(S,K,E) problem: DPs: TRS: ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) -> ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) -> choice(S,cons(u,K),E) choice(cons(u,S),K,E) -> choice(S,K,E) Qed DPs: complete#(u,cons(v,S),E) -> complete#(u,S,E) TRS: ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) -> ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) -> choice(S,cons(u,K),E) choice(cons(u,S),K,E) -> choice(S,K,E) Matrix Interpretation Processor: dimension: 1 interpretation: [complete#](x0, x1, x2) = x1 + 1, [choice](x0, x1, x2) = x0 + x1, [clique](x0, x1) = 0, [complete](x0, x1, x2) = 0, [cons](x0, x1) = x1 + 1, [find](x0, x1, x2) = 0, [nil] = 0, [ff] = 0, [ite](x0, x1, x2) = x1 + x2, [tt] = 0 orientation: complete#(u,cons(v,S),E) = S + 2 >= S + 1 = complete#(u,S,E) ite(tt(),u,v) = u + v >= u = u ite(ff(),u,v) = u + v >= v = v find(u,v,nil()) = 0 >= 0 = ff() find(u,v,cons(cons(u,v),E)) = 0 >= 0 = tt() find(u,v,cons(cons(u2,v2),E)) = 0 >= 0 = find(u,v,E) complete(u,nil(),E) = 0 >= 0 = tt() complete(u,cons(v,S),E) = 0 >= 0 = ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) = 0 >= 0 = tt() clique(cons(u,K),E) = 0 >= 0 = ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) = K >= K = ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) = K + S + 1 >= K + S + 1 = choice(S,cons(u,K),E) choice(cons(u,S),K,E) = K + S + 1 >= K + S = choice(S,K,E) problem: DPs: TRS: ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) -> ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) -> choice(S,cons(u,K),E) choice(cons(u,S),K,E) -> choice(S,K,E) Qed DPs: find#(u,v,cons(cons(u2,v2),E)) -> find#(u,v,E) TRS: ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) -> ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) -> choice(S,cons(u,K),E) choice(cons(u,S),K,E) -> choice(S,K,E) Matrix Interpretation Processor: dimension: 1 interpretation: [find#](x0, x1, x2) = x2, [choice](x0, x1, x2) = x0 + x1, [clique](x0, x1) = 0, [complete](x0, x1, x2) = 0, [cons](x0, x1) = x0 + x1 + 1, [find](x0, x1, x2) = 1, [nil] = 0, [ff] = 0, [ite](x0, x1, x2) = x1 + x2, [tt] = 0 orientation: find#(u,v,cons(cons(u2,v2),E)) = E + u2 + v2 + 2 >= E = find#(u,v,E) ite(tt(),u,v) = u + v >= u = u ite(ff(),u,v) = u + v >= v = v find(u,v,nil()) = 1 >= 0 = ff() find(u,v,cons(cons(u,v),E)) = 1 >= 0 = tt() find(u,v,cons(cons(u2,v2),E)) = 1 >= 1 = find(u,v,E) complete(u,nil(),E) = 0 >= 0 = tt() complete(u,cons(v,S),E) = 0 >= 0 = ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) = 0 >= 0 = tt() clique(cons(u,K),E) = 0 >= 0 = ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) = K >= K = ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) = K + S + u + 1 >= K + S + u + 1 = choice(S,cons(u,K),E) choice(cons(u,S),K,E) = K + S + u + 1 >= K + S = choice(S,K,E) problem: DPs: TRS: ite(tt(),u,v) -> u ite(ff(),u,v) -> v find(u,v,nil()) -> ff() find(u,v,cons(cons(u,v),E)) -> tt() find(u,v,cons(cons(u2,v2),E)) -> find(u,v,E) complete(u,nil(),E) -> tt() complete(u,cons(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff()) clique(nil(),E) -> tt() clique(cons(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff()) choice(nil(),K,E) -> ite(clique(K,E),K,nil()) choice(cons(u,S),K,E) -> choice(S,cons(u,K),E) choice(cons(u,S),K,E) -> choice(S,K,E) Qed