MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. 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()) , choice(nil(), K, E) -> ite(clique(K, E), K, nil()) , choice(cons(u, S), K, E) -> choice(S, K, E) , choice(cons(u, S), K, E) -> choice(S, cons(u, K), E) } Obligation: innermost runtime complexity Answer: MAYBE 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)) , choice^#(nil(), K, E) -> c_10(ite^#(clique(K, E), K, nil()), clique^#(K, E)) , choice^#(cons(u, S), K, E) -> c_11(choice^#(S, K, E)) , choice^#(cons(u, S), K, E) -> c_12(choice^#(S, cons(u, K), E)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. 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)) , choice^#(nil(), K, E) -> c_10(ite^#(clique(K, E), K, nil()), clique^#(K, E)) , choice^#(cons(u, S), K, E) -> c_11(choice^#(S, K, E)) , choice^#(cons(u, S), K, E) -> c_12(choice^#(S, cons(u, 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()) , choice(nil(), K, E) -> ite(clique(K, E), K, nil()) , choice(cons(u, S), K, E) -> choice(S, K, E) , choice(cons(u, S), K, E) -> choice(S, cons(u, K), E) } Obligation: innermost runtime complexity Answer: MAYBE 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,10}. 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)) , 10: choice^#(nil(), K, E) -> c_10(ite^#(clique(K, E), K, nil()), clique^#(K, E)) , 11: choice^#(cons(u, S), K, E) -> c_11(choice^#(S, K, E)) , 12: choice^#(cons(u, S), K, E) -> c_12(choice^#(S, cons(u, K), E)) } We are left with following problem, upon which TcT provides the certificate MAYBE. 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)) , choice^#(nil(), K, E) -> c_10(ite^#(clique(K, E), K, nil()), clique^#(K, E)) , choice^#(cons(u, S), K, E) -> c_11(choice^#(S, K, E)) , choice^#(cons(u, S), K, E) -> c_12(choice^#(S, cons(u, 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()) , choice(nil(), K, E) -> ite(clique(K, E), K, nil()) , choice(cons(u, S), K, E) -> choice(S, K, E) , choice(cons(u, S), K, E) -> choice(S, cons(u, K), E) } Obligation: innermost runtime complexity Answer: MAYBE 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 MAYBE. 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)) , choice^#(nil(), K, E) -> c_10(ite^#(clique(K, E), K, nil()), clique^#(K, E)) , choice^#(cons(u, S), K, E) -> c_11(choice^#(S, K, E)) , choice^#(cons(u, S), K, E) -> c_12(choice^#(S, cons(u, 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()) , choice(nil(), K, E) -> ite(clique(K, E), K, nil()) , choice(cons(u, S), K, E) -> choice(S, K, E) , choice(cons(u, S), K, E) -> choice(S, cons(u, K), E) } Obligation: innermost runtime complexity Answer: MAYBE 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)) , choice^#(nil(), K, E) -> c_10(ite^#(clique(K, E), K, nil()), clique^#(K, E)) } We are left with following problem, upon which TcT provides the certificate MAYBE. 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)) , choice^#(nil(), K, E) -> c_4(clique^#(K, E)) , choice^#(cons(u, S), K, E) -> c_5(choice^#(S, K, E)) , choice^#(cons(u, S), K, E) -> c_6(choice^#(S, cons(u, 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()) , choice(nil(), K, E) -> ite(clique(K, E), K, nil()) , choice(cons(u, S), K, E) -> choice(S, K, E) , choice(cons(u, S), K, E) -> choice(S, cons(u, K), E) } Obligation: innermost runtime complexity Answer: MAYBE No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate MAYBE. 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)) , choice^#(nil(), K, E) -> c_4(clique^#(K, E)) , choice^#(cons(u, S), K, E) -> c_5(choice^#(S, K, E)) , choice^#(cons(u, S), K, E) -> c_6(choice^#(S, cons(u, K), E)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrices' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrix interpretation of dimension 4' failed due to the following reason: The input cannot be shown compatible 2) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 3) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 4) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 5) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 6) 'matrix interpretation of dimension 1' failed due to the following reason: The input cannot be shown compatible 2) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. Arrrr..