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()) 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()) 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()) TDG 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()) 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()) graph: 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) -> 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) -> clique#(K,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()) 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) -> complete#(u,S,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) -> 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) -> complete#(u,S,E) 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) SCC Processor: #sccs: 3 #rules: 3 #arcs: 11/49 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()) Subterm Criterion Processor: simple projection: pi(clique#) = 0 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()) 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()) Subterm Criterion Processor: simple projection: pi(complete#) = 1 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()) 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()) Subterm Criterion Processor: simple projection: pi(find#) = 2 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()) Qed