MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { log(x, s(s(y))) -> cond(le(x, s(s(y))), x, y) , cond(true(), x, y) -> s(0()) , cond(false(), x, y) -> double(log(x, square(s(s(y))))) , le(s(u), s(v)) -> le(u, v) , le(s(u), 0()) -> false() , le(0(), v) -> true() , double(s(x)) -> s(s(double(x))) , double(0()) -> 0() , square(s(x)) -> s(plus(square(x), double(x))) , square(0()) -> 0() , plus(n, s(m)) -> s(plus(n, m)) , plus(n, 0()) -> n } 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: { log^#(x, s(s(y))) -> c_1(cond^#(le(x, s(s(y))), x, y)) , cond^#(true(), x, y) -> c_2() , cond^#(false(), x, y) -> c_3(double^#(log(x, square(s(s(y)))))) , double^#(s(x)) -> c_7(double^#(x)) , double^#(0()) -> c_8() , le^#(s(u), s(v)) -> c_4(le^#(u, v)) , le^#(s(u), 0()) -> c_5() , le^#(0(), v) -> c_6() , square^#(s(x)) -> c_9(plus^#(square(x), double(x))) , square^#(0()) -> c_10() , plus^#(n, s(m)) -> c_11(plus^#(n, m)) , plus^#(n, 0()) -> c_12(n) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { log^#(x, s(s(y))) -> c_1(cond^#(le(x, s(s(y))), x, y)) , cond^#(true(), x, y) -> c_2() , cond^#(false(), x, y) -> c_3(double^#(log(x, square(s(s(y)))))) , double^#(s(x)) -> c_7(double^#(x)) , double^#(0()) -> c_8() , le^#(s(u), s(v)) -> c_4(le^#(u, v)) , le^#(s(u), 0()) -> c_5() , le^#(0(), v) -> c_6() , square^#(s(x)) -> c_9(plus^#(square(x), double(x))) , square^#(0()) -> c_10() , plus^#(n, s(m)) -> c_11(plus^#(n, m)) , plus^#(n, 0()) -> c_12(n) } Strict Trs: { log(x, s(s(y))) -> cond(le(x, s(s(y))), x, y) , cond(true(), x, y) -> s(0()) , cond(false(), x, y) -> double(log(x, square(s(s(y))))) , le(s(u), s(v)) -> le(u, v) , le(s(u), 0()) -> false() , le(0(), v) -> true() , double(s(x)) -> s(s(double(x))) , double(0()) -> 0() , square(s(x)) -> s(plus(square(x), double(x))) , square(0()) -> 0() , plus(n, s(m)) -> s(plus(n, m)) , plus(n, 0()) -> n } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {2,5,7,8,10} by applications of Pre({2,5,7,8,10}) = {1,3,4,6,12}. Here rules are labeled as follows: DPs: { 1: log^#(x, s(s(y))) -> c_1(cond^#(le(x, s(s(y))), x, y)) , 2: cond^#(true(), x, y) -> c_2() , 3: cond^#(false(), x, y) -> c_3(double^#(log(x, square(s(s(y)))))) , 4: double^#(s(x)) -> c_7(double^#(x)) , 5: double^#(0()) -> c_8() , 6: le^#(s(u), s(v)) -> c_4(le^#(u, v)) , 7: le^#(s(u), 0()) -> c_5() , 8: le^#(0(), v) -> c_6() , 9: square^#(s(x)) -> c_9(plus^#(square(x), double(x))) , 10: square^#(0()) -> c_10() , 11: plus^#(n, s(m)) -> c_11(plus^#(n, m)) , 12: plus^#(n, 0()) -> c_12(n) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { log^#(x, s(s(y))) -> c_1(cond^#(le(x, s(s(y))), x, y)) , cond^#(false(), x, y) -> c_3(double^#(log(x, square(s(s(y)))))) , double^#(s(x)) -> c_7(double^#(x)) , le^#(s(u), s(v)) -> c_4(le^#(u, v)) , square^#(s(x)) -> c_9(plus^#(square(x), double(x))) , plus^#(n, s(m)) -> c_11(plus^#(n, m)) , plus^#(n, 0()) -> c_12(n) } Strict Trs: { log(x, s(s(y))) -> cond(le(x, s(s(y))), x, y) , cond(true(), x, y) -> s(0()) , cond(false(), x, y) -> double(log(x, square(s(s(y))))) , le(s(u), s(v)) -> le(u, v) , le(s(u), 0()) -> false() , le(0(), v) -> true() , double(s(x)) -> s(s(double(x))) , double(0()) -> 0() , square(s(x)) -> s(plus(square(x), double(x))) , square(0()) -> 0() , plus(n, s(m)) -> s(plus(n, m)) , plus(n, 0()) -> n } Weak DPs: { cond^#(true(), x, y) -> c_2() , double^#(0()) -> c_8() , le^#(s(u), 0()) -> c_5() , le^#(0(), v) -> c_6() , square^#(0()) -> c_10() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..