Problem TCT 09 ma6

TIMEOUT

We are left with following problem, upon which TcT provides the
certificate TIMEOUT.

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:
  TIMEOUT

Computation stopped due to timeout after 20.0 seconds.

Arrrr..

YES(?,ELEMENTARY)

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

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

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

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

and precedence

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

Following symbols are considered recursive:

 {ite, find, complete, clique}

The recursion depth is 3.

For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:

 Strict DPs: 
 Weak DPs  : 
 Strict Trs:
   { ite(v; tt(),  u) -> u
   , ite(v; ff(),  u) -> 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(ff(); find(u,  v,  E;),  complete(u,  S,  E;))
   , clique(nil(),  E;) -> tt()
   , clique(cons(; u,  K),  E;) ->
     ite(ff(); complete(u,  K,  E;),  clique(K,  E;)) }
 Weak Trs  : 

Hurray, we answered YES(?,ELEMENTARY)

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 orders'
as induced by the precedence

 find > tt, nil > tt, nil > ff, cons > ff, complete > ite,
 clique > ite, clique > complete, find ~ complete .

Hurray, we answered YES(?,PRIMREC)

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}, safe(tt) = {}, safe(ff) = {},
 safe(find) = {1, 2}, safe(nil) = {}, safe(cons) = {1, 2},
 safe(complete) = {1}, safe(clique) = {}

and precedence

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

Following symbols are considered recursive:

 {ite, find, complete, clique}

The recursion depth is 3.

For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:

 Strict DPs: 
 Weak DPs  : 
 Strict Trs:
   { ite(v; tt(),  u) -> u
   , ite(v; ff(),  u) -> 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(ff(); find(E; u,  v),  complete(S,  E; u))
   , clique(nil(),  E;) -> tt()
   , clique(cons(; u,  K),  E;) ->
     ite(ff(); complete(K,  E; u),  clique(K,  E;)) }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)

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
(PS)' as induced by the safe mapping

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

and precedence

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

Following symbols are considered recursive:

 {ite, find, complete, clique}

The recursion depth is 3.

For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:

 Strict DPs: 
 Weak DPs  : 
 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()) }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)