YES(?,POLY)

We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).

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(?,POLY)

The input was oriented with the instance of 'Polynomial Path Order'
as induced by the safe mapping

 safe(ite) = {1, 2, 3}, safe(tt) = {}, safe(ff) = {},
 safe(find) = {1, 2}, safe(nil) = {}, safe(cons) = {1, 2},
 safe(complete) = {}, safe(clique) = {}

and precedence

 find > ite, complete > ite, complete > find, clique > ite,
 clique > find, clique > complete .

Following symbols are considered recursive:

 {ite, find, complete, clique}

The recursion depth is 4.

For your convenience, here are the satisfied ordering constraints:

                       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(u,  nil(),  E;) > tt()                                               
                                                                                                
          complete(u,  cons(; v,  S),  E;) > ite(; find(E; u,  v),  complete(u,  S,  E;),  ff())
                                                                                                
                        clique(nil(),  E;) > tt()                                               
                                                                                                
                clique(cons(; u,  K),  E;) > ite(; complete(u,  K,  E;),  clique(K,  E;),  ff())
                                                                                                

Hurray, we answered YES(?,POLY)