YES(?,O(n^3))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^3)).

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(?,O(n^3))

We add following dependency tuples:

Strict DPs:
  { ite^#(tt(), u, v) -> c_1()
  , ite^#(ff(), u, v) -> c_2()
  , find^#(u, v, nil()) -> c_3()
  , find^#(u, v, cons(cons(u, v), E)) -> c_4()
  , find^#(u, v, cons(cons(u2, v2), E)) -> c_5(find^#(u, v, E))
  , complete^#(u, nil(), E) -> c_6()
  , complete^#(u, cons(v, S), E) ->
    c_7(ite^#(find(u, v, E), complete(u, S, E), ff()),
        find^#(u, v, E),
        complete^#(u, S, E))
  , clique^#(nil(), E) -> c_8()
  , clique^#(cons(u, K), E) ->
    c_9(ite^#(complete(u, K, E), clique(K, E), ff()),
        complete^#(u, K, E),
        clique^#(K, E)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^3)).

Strict DPs:
  { ite^#(tt(), u, v) -> c_1()
  , ite^#(ff(), u, v) -> c_2()
  , find^#(u, v, nil()) -> c_3()
  , find^#(u, v, cons(cons(u, v), E)) -> c_4()
  , find^#(u, v, cons(cons(u2, v2), E)) -> c_5(find^#(u, v, E))
  , complete^#(u, nil(), E) -> c_6()
  , complete^#(u, cons(v, S), E) ->
    c_7(ite^#(find(u, v, E), complete(u, S, E), ff()),
        find^#(u, v, E),
        complete^#(u, S, E))
  , clique^#(nil(), E) -> c_8()
  , clique^#(cons(u, K), E) ->
    c_9(ite^#(complete(u, K, E), clique(K, E), ff()),
        complete^#(u, K, E),
        clique^#(K, E)) }
Weak 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(?,O(n^3))

We estimate the number of application of {1,2,3,4,6,8} by
applications of Pre({1,2,3,4,6,8}) = {5,7,9}. Here rules are
labeled as follows:

  DPs:
    { 1: ite^#(tt(), u, v) -> c_1()
    , 2: ite^#(ff(), u, v) -> c_2()
    , 3: find^#(u, v, nil()) -> c_3()
    , 4: find^#(u, v, cons(cons(u, v), E)) -> c_4()
    , 5: find^#(u, v, cons(cons(u2, v2), E)) -> c_5(find^#(u, v, E))
    , 6: complete^#(u, nil(), E) -> c_6()
    , 7: complete^#(u, cons(v, S), E) ->
         c_7(ite^#(find(u, v, E), complete(u, S, E), ff()),
             find^#(u, v, E),
             complete^#(u, S, E))
    , 8: clique^#(nil(), E) -> c_8()
    , 9: clique^#(cons(u, K), E) ->
         c_9(ite^#(complete(u, K, E), clique(K, E), ff()),
             complete^#(u, K, E),
             clique^#(K, E)) }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^3)).

Strict DPs:
  { find^#(u, v, cons(cons(u2, v2), E)) -> c_5(find^#(u, v, E))
  , complete^#(u, cons(v, S), E) ->
    c_7(ite^#(find(u, v, E), complete(u, S, E), ff()),
        find^#(u, v, E),
        complete^#(u, S, E))
  , clique^#(cons(u, K), E) ->
    c_9(ite^#(complete(u, K, E), clique(K, E), ff()),
        complete^#(u, K, E),
        clique^#(K, E)) }
Weak DPs:
  { ite^#(tt(), u, v) -> c_1()
  , ite^#(ff(), u, v) -> c_2()
  , find^#(u, v, nil()) -> c_3()
  , find^#(u, v, cons(cons(u, v), E)) -> c_4()
  , complete^#(u, nil(), E) -> c_6()
  , clique^#(nil(), E) -> c_8() }
Weak 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(?,O(n^3))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ ite^#(tt(), u, v) -> c_1()
, ite^#(ff(), u, v) -> c_2()
, find^#(u, v, nil()) -> c_3()
, find^#(u, v, cons(cons(u, v), E)) -> c_4()
, complete^#(u, nil(), E) -> c_6()
, clique^#(nil(), E) -> c_8() }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^3)).

Strict DPs:
  { find^#(u, v, cons(cons(u2, v2), E)) -> c_5(find^#(u, v, E))
  , complete^#(u, cons(v, S), E) ->
    c_7(ite^#(find(u, v, E), complete(u, S, E), ff()),
        find^#(u, v, E),
        complete^#(u, S, E))
  , clique^#(cons(u, K), E) ->
    c_9(ite^#(complete(u, K, E), clique(K, E), ff()),
        complete^#(u, K, E),
        clique^#(K, E)) }
Weak 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(?,O(n^3))

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { complete^#(u, cons(v, S), E) ->
    c_7(ite^#(find(u, v, E), complete(u, S, E), ff()),
        find^#(u, v, E),
        complete^#(u, S, E))
  , clique^#(cons(u, K), E) ->
    c_9(ite^#(complete(u, K, E), clique(K, E), ff()),
        complete^#(u, K, E),
        clique^#(K, E)) }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^3)).

Strict DPs:
  { find^#(u, v, cons(cons(u2, v2), E)) -> c_1(find^#(u, v, E))
  , complete^#(u, cons(v, S), E) ->
    c_2(find^#(u, v, E), complete^#(u, S, E))
  , clique^#(cons(u, K), E) ->
    c_3(complete^#(u, K, E), clique^#(K, E)) }
Weak 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(?,O(n^3))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^3)).

Strict DPs:
  { find^#(u, v, cons(cons(u2, v2), E)) -> c_1(find^#(u, v, E))
  , complete^#(u, cons(v, S), E) ->
    c_2(find^#(u, v, E), complete^#(u, S, E))
  , clique^#(cons(u, K), E) ->
    c_3(complete^#(u, K, E), clique^#(K, E)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^3))

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

 safe(cons) = {1, 2}, safe(find^#) = {2}, safe(complete^#) = {},
 safe(clique^#) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}

and precedence

 complete^# > find^#, clique^# > find^#, clique^# > complete^# .

Following symbols are considered recursive:

 {find^#, complete^#, clique^#}

The recursion depth is 3.

Further, following argument filtering is employed:

 pi(cons) = [1, 2], pi(find^#) = [1, 2, 3],
 pi(complete^#) = [1, 2, 3], pi(clique^#) = [1, 2], pi(c_1) = [1],
 pi(c_2) = [1, 2], pi(c_3) = [1, 2]

Usable defined function symbols are a subset of:

 {find^#, complete^#, clique^#}

For your convenience, here are the satisfied ordering constraints:

  pi(find^#(u, v, cons(cons(u2, v2), E))) = find^#(u,  cons(; cons(; u2,  v2),  E); v)     
                                          > c_1(find^#(u,  E; v);)                         
                                          = pi(c_1(find^#(u, v, E)))                       
                                                                                           
         pi(complete^#(u, cons(v, S), E)) = complete^#(u,  cons(; v,  S),  E;)             
                                          > c_2(find^#(u,  E; v),  complete^#(u,  S,  E;);)
                                          = pi(c_2(find^#(u, v, E), complete^#(u, S, E)))  
                                                                                           
              pi(clique^#(cons(u, K), E)) = clique^#(cons(; u,  K),  E;)                   
                                          > c_3(complete^#(u,  K,  E;),  clique^#(K,  E;);)
                                          = pi(c_3(complete^#(u, K, E), clique^#(K, E)))   
                                                                                           

Hurray, we answered YES(?,O(n^3))