MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { eq(0(), 0()) -> true() , eq(0(), s(x)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , or(true(), y) -> true() , or(false(), y) -> y , and(true(), y) -> y , and(false(), y) -> false() , size(empty()) -> 0() , size(edge(x, y, i)) -> s(size(i)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , reachable(x, y, i) -> reach(x, y, 0(), i, i) , reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j) , if1(true(), x, y, c, i, j) -> true() , if1(false(), x, y, c, i, j) -> if2(le(c, size(j)), x, y, c, i, j) , if2(true(), x, y, c, empty(), j) -> false() , if2(true(), x, y, c, edge(u, v, i), j) -> or(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j))) , if2(false(), x, y, c, i, j) -> false() } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { eq^#(0(), 0()) -> c_1() , eq^#(0(), s(x)) -> c_2() , eq^#(s(x), 0()) -> c_3() , eq^#(s(x), s(y)) -> c_4(eq^#(x, y)) , or^#(true(), y) -> c_5() , or^#(false(), y) -> c_6(y) , and^#(true(), y) -> c_7(y) , and^#(false(), y) -> c_8() , size^#(empty()) -> c_9() , size^#(edge(x, y, i)) -> c_10(size^#(i)) , le^#(0(), y) -> c_11() , le^#(s(x), 0()) -> c_12() , le^#(s(x), s(y)) -> c_13(le^#(x, y)) , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i)) , reach^#(x, y, c, i, j) -> c_15(if1^#(eq(x, y), x, y, c, i, j)) , if1^#(true(), x, y, c, i, j) -> c_16() , if1^#(false(), x, y, c, i, j) -> c_17(if2^#(le(c, size(j)), x, y, c, i, j)) , if2^#(true(), x, y, c, empty(), j) -> c_18() , if2^#(true(), x, y, c, edge(u, v, i), j) -> c_19(or^#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))) , if2^#(false(), x, y, c, i, j) -> c_20() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { eq^#(0(), 0()) -> c_1() , eq^#(0(), s(x)) -> c_2() , eq^#(s(x), 0()) -> c_3() , eq^#(s(x), s(y)) -> c_4(eq^#(x, y)) , or^#(true(), y) -> c_5() , or^#(false(), y) -> c_6(y) , and^#(true(), y) -> c_7(y) , and^#(false(), y) -> c_8() , size^#(empty()) -> c_9() , size^#(edge(x, y, i)) -> c_10(size^#(i)) , le^#(0(), y) -> c_11() , le^#(s(x), 0()) -> c_12() , le^#(s(x), s(y)) -> c_13(le^#(x, y)) , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i)) , reach^#(x, y, c, i, j) -> c_15(if1^#(eq(x, y), x, y, c, i, j)) , if1^#(true(), x, y, c, i, j) -> c_16() , if1^#(false(), x, y, c, i, j) -> c_17(if2^#(le(c, size(j)), x, y, c, i, j)) , if2^#(true(), x, y, c, empty(), j) -> c_18() , if2^#(true(), x, y, c, edge(u, v, i), j) -> c_19(or^#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))) , if2^#(false(), x, y, c, i, j) -> c_20() } Strict Trs: { eq(0(), 0()) -> true() , eq(0(), s(x)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , or(true(), y) -> true() , or(false(), y) -> y , and(true(), y) -> y , and(false(), y) -> false() , size(empty()) -> 0() , size(edge(x, y, i)) -> s(size(i)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , reachable(x, y, i) -> reach(x, y, 0(), i, i) , reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j) , if1(true(), x, y, c, i, j) -> true() , if1(false(), x, y, c, i, j) -> if2(le(c, size(j)), x, y, c, i, j) , if2(true(), x, y, c, empty(), j) -> false() , if2(true(), x, y, c, edge(u, v, i), j) -> or(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j))) , if2(false(), x, y, c, i, j) -> false() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,5,8,9,11,12,16,18,20} by applications of Pre({1,2,3,5,8,9,11,12,16,18,20}) = {4,6,7,10,13,15,17,19}. Here rules are labeled as follows: DPs: { 1: eq^#(0(), 0()) -> c_1() , 2: eq^#(0(), s(x)) -> c_2() , 3: eq^#(s(x), 0()) -> c_3() , 4: eq^#(s(x), s(y)) -> c_4(eq^#(x, y)) , 5: or^#(true(), y) -> c_5() , 6: or^#(false(), y) -> c_6(y) , 7: and^#(true(), y) -> c_7(y) , 8: and^#(false(), y) -> c_8() , 9: size^#(empty()) -> c_9() , 10: size^#(edge(x, y, i)) -> c_10(size^#(i)) , 11: le^#(0(), y) -> c_11() , 12: le^#(s(x), 0()) -> c_12() , 13: le^#(s(x), s(y)) -> c_13(le^#(x, y)) , 14: reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i)) , 15: reach^#(x, y, c, i, j) -> c_15(if1^#(eq(x, y), x, y, c, i, j)) , 16: if1^#(true(), x, y, c, i, j) -> c_16() , 17: if1^#(false(), x, y, c, i, j) -> c_17(if2^#(le(c, size(j)), x, y, c, i, j)) , 18: if2^#(true(), x, y, c, empty(), j) -> c_18() , 19: if2^#(true(), x, y, c, edge(u, v, i), j) -> c_19(or^#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))) , 20: if2^#(false(), x, y, c, i, j) -> c_20() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { eq^#(s(x), s(y)) -> c_4(eq^#(x, y)) , or^#(false(), y) -> c_6(y) , and^#(true(), y) -> c_7(y) , size^#(edge(x, y, i)) -> c_10(size^#(i)) , le^#(s(x), s(y)) -> c_13(le^#(x, y)) , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i)) , reach^#(x, y, c, i, j) -> c_15(if1^#(eq(x, y), x, y, c, i, j)) , if1^#(false(), x, y, c, i, j) -> c_17(if2^#(le(c, size(j)), x, y, c, i, j)) , if2^#(true(), x, y, c, edge(u, v, i), j) -> c_19(or^#(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))) } Strict Trs: { eq(0(), 0()) -> true() , eq(0(), s(x)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , or(true(), y) -> true() , or(false(), y) -> y , and(true(), y) -> y , and(false(), y) -> false() , size(empty()) -> 0() , size(edge(x, y, i)) -> s(size(i)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , reachable(x, y, i) -> reach(x, y, 0(), i, i) , reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j) , if1(true(), x, y, c, i, j) -> true() , if1(false(), x, y, c, i, j) -> if2(le(c, size(j)), x, y, c, i, j) , if2(true(), x, y, c, empty(), j) -> false() , if2(true(), x, y, c, edge(u, v, i), j) -> or(if2(true(), x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j))) , if2(false(), x, y, c, i, j) -> false() } Weak DPs: { eq^#(0(), 0()) -> c_1() , eq^#(0(), s(x)) -> c_2() , eq^#(s(x), 0()) -> c_3() , or^#(true(), y) -> c_5() , and^#(false(), y) -> c_8() , size^#(empty()) -> c_9() , le^#(0(), y) -> c_11() , le^#(s(x), 0()) -> c_12() , if1^#(true(), x, y, c, i, j) -> c_16() , if2^#(true(), x, y, c, empty(), j) -> c_18() , if2^#(false(), x, y, c, i, j) -> c_20() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..