YES(?,POLY) 'Pop* with parameter subtitution (timeout of 60.0 seconds)' ----------------------------------------------------------- Answer: YES(?,POLY) Input Problem: innermost runtime-complexity with respect to Rules: { 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 Output: The input was oriented with the instance of POP* as induced by the precedence find > ite, complete > ite, complete > find, clique > ite, clique > find, clique > complete and safe mapping safe(ite) = {1, 2, 3}, safe(tt) = {}, safe(ff) = {}, safe(find) = {1, 2}, safe(nil) = {}, safe(cons) = {1, 2}, safe(complete) = {1}, safe(clique) = {} . For your convenience, here is the input in predicative notation: Rules: { ite(; tt(), u, v) -> u , ite(; ff(), u, v) -> v , find(nil(); u, v) -> ff() , find(cons(; cons(; u, v), E); u, v) -> tt() , find(cons(; cons(; u2, v2), E); u, v) -> find(E; u, v) , complete(nil(), E; u) -> tt() , complete(cons(; v, S), E; u) -> ite(; find(E; u, v), complete(S, E; u), ff()) , clique(nil(), E;) -> tt() , clique(cons(; u, K), E;) -> ite(; complete(K, E; u), clique(K, E;), ff())}