YES(?,PRIMREC) We are left with following problem, upon which TcT provides the certificate YES(?,PRIMREC). Strict 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()) } Obligation: innermost runtime complexity Answer: YES(?,PRIMREC) The input was oriented with the instance of'multiset path order' as induced by the precedence ite > tt, ite > ff, ite > find, ite > cons, find > tt, find > ff, find > cons, nil > ite, nil > tt, nil > find, nil > cons, nil > complete, nil > clique, complete > ite, complete > find, complete > cons, clique > ite, clique > tt, clique > ff, clique > find, clique > cons, clique > complete, tt ~ ff, ff ~ cons . Hurray, we answered YES(?,PRIMREC)