MAYBE 880.04/295.40 MAYBE 880.04/295.40 880.04/295.40 We are left with following problem, upon which TcT provides the 880.04/295.40 certificate MAYBE. 880.04/295.40 880.04/295.40 Strict Trs: 880.04/295.40 { log(x, s(s(y))) -> cond(le(x, s(s(y))), x, y) 880.04/295.40 , cond(true(), x, y) -> s(0()) 880.04/295.40 , cond(false(), x, y) -> double(log(x, square(s(s(y))))) 880.04/295.40 , le(s(u), s(v)) -> le(u, v) 880.04/295.40 , le(s(u), 0()) -> false() 880.04/295.40 , le(0(), v) -> true() 880.04/295.40 , double(s(x)) -> s(s(double(x))) 880.04/295.40 , double(0()) -> 0() 880.04/295.40 , square(s(x)) -> s(plus(square(x), double(x))) 880.04/295.40 , square(0()) -> 0() 880.04/295.40 , plus(n, s(m)) -> s(plus(n, m)) 880.04/295.40 , plus(n, 0()) -> n } 880.04/295.40 Obligation: 880.04/295.40 runtime complexity 880.04/295.40 Answer: 880.04/295.40 MAYBE 880.04/295.40 880.04/295.40 None of the processors succeeded. 880.04/295.40 880.04/295.40 Details of failed attempt(s): 880.04/295.40 ----------------------------- 880.04/295.40 1) 'Best' failed due to the following reason: 880.04/295.40 880.04/295.40 None of the processors succeeded. 880.04/295.40 880.04/295.40 Details of failed attempt(s): 880.04/295.40 ----------------------------- 880.04/295.40 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 880.04/295.40 seconds)' failed due to the following reason: 880.04/295.40 880.04/295.40 Computation stopped due to timeout after 148.0 seconds. 880.04/295.40 880.04/295.40 2) 'Best' failed due to the following reason: 880.04/295.40 880.04/295.40 None of the processors succeeded. 880.04/295.40 880.04/295.40 Details of failed attempt(s): 880.04/295.40 ----------------------------- 880.04/295.40 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 880.04/295.40 to the following reason: 880.04/295.40 880.04/295.40 The processor is inapplicable, reason: 880.04/295.40 Processor only applicable for innermost runtime complexity analysis 880.04/295.40 880.04/295.40 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 880.04/295.40 following reason: 880.04/295.40 880.04/295.40 The processor is inapplicable, reason: 880.04/295.40 Processor only applicable for innermost runtime complexity analysis 880.04/295.40 880.04/295.40 880.04/295.40 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 880.04/295.40 failed due to the following reason: 880.04/295.40 880.04/295.40 None of the processors succeeded. 880.04/295.40 880.04/295.40 Details of failed attempt(s): 880.04/295.40 ----------------------------- 880.04/295.40 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 880.04/295.40 failed due to the following reason: 880.04/295.40 880.04/295.40 match-boundness of the problem could not be verified. 880.04/295.40 880.04/295.40 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 880.04/295.40 failed due to the following reason: 880.04/295.40 880.04/295.40 match-boundness of the problem could not be verified. 880.04/295.40 880.04/295.40 880.04/295.40 880.04/295.40 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 880.04/295.40 the following reason: 880.04/295.40 880.04/295.40 We add the following weak dependency pairs: 880.04/295.40 880.04/295.40 Strict DPs: 880.04/295.40 { log^#(x, s(s(y))) -> c_1(cond^#(le(x, s(s(y))), x, y)) 880.04/295.40 , cond^#(true(), x, y) -> c_2() 880.04/295.40 , cond^#(false(), x, y) -> c_3(double^#(log(x, square(s(s(y)))))) 880.04/295.40 , double^#(s(x)) -> c_7(double^#(x)) 880.04/295.40 , double^#(0()) -> c_8() 880.04/295.40 , le^#(s(u), s(v)) -> c_4(le^#(u, v)) 880.04/295.40 , le^#(s(u), 0()) -> c_5() 880.04/295.40 , le^#(0(), v) -> c_6() 880.04/295.40 , square^#(s(x)) -> c_9(plus^#(square(x), double(x))) 880.04/295.40 , square^#(0()) -> c_10() 880.04/295.40 , plus^#(n, s(m)) -> c_11(plus^#(n, m)) 880.04/295.40 , plus^#(n, 0()) -> c_12(n) } 880.04/295.40 880.04/295.40 and mark the set of starting terms. 880.04/295.40 880.04/295.40 We are left with following problem, upon which TcT provides the 880.04/295.40 certificate MAYBE. 880.04/295.40 880.04/295.40 Strict DPs: 880.04/295.40 { log^#(x, s(s(y))) -> c_1(cond^#(le(x, s(s(y))), x, y)) 880.04/295.40 , cond^#(true(), x, y) -> c_2() 880.04/295.40 , cond^#(false(), x, y) -> c_3(double^#(log(x, square(s(s(y)))))) 880.04/295.40 , double^#(s(x)) -> c_7(double^#(x)) 880.04/295.40 , double^#(0()) -> c_8() 880.04/295.40 , le^#(s(u), s(v)) -> c_4(le^#(u, v)) 880.04/295.40 , le^#(s(u), 0()) -> c_5() 880.04/295.40 , le^#(0(), v) -> c_6() 880.04/295.40 , square^#(s(x)) -> c_9(plus^#(square(x), double(x))) 880.04/295.40 , square^#(0()) -> c_10() 880.04/295.40 , plus^#(n, s(m)) -> c_11(plus^#(n, m)) 880.04/295.40 , plus^#(n, 0()) -> c_12(n) } 880.04/295.40 Strict Trs: 880.04/295.40 { log(x, s(s(y))) -> cond(le(x, s(s(y))), x, y) 880.04/295.40 , cond(true(), x, y) -> s(0()) 880.04/295.40 , cond(false(), x, y) -> double(log(x, square(s(s(y))))) 880.04/295.40 , le(s(u), s(v)) -> le(u, v) 880.04/295.40 , le(s(u), 0()) -> false() 880.04/295.40 , le(0(), v) -> true() 880.04/295.40 , double(s(x)) -> s(s(double(x))) 880.04/295.40 , double(0()) -> 0() 880.04/295.40 , square(s(x)) -> s(plus(square(x), double(x))) 880.04/295.40 , square(0()) -> 0() 880.04/295.40 , plus(n, s(m)) -> s(plus(n, m)) 880.04/295.40 , plus(n, 0()) -> n } 880.04/295.40 Obligation: 880.04/295.40 runtime complexity 880.04/295.40 Answer: 880.04/295.40 MAYBE 880.04/295.40 880.04/295.40 We estimate the number of application of {2,5,7,8,10} by 880.04/295.40 applications of Pre({2,5,7,8,10}) = {1,3,4,6,12}. Here rules are 880.04/295.40 labeled as follows: 880.04/295.40 880.04/295.40 DPs: 880.04/295.40 { 1: log^#(x, s(s(y))) -> c_1(cond^#(le(x, s(s(y))), x, y)) 880.04/295.40 , 2: cond^#(true(), x, y) -> c_2() 880.04/295.40 , 3: cond^#(false(), x, y) -> 880.04/295.40 c_3(double^#(log(x, square(s(s(y)))))) 880.04/295.40 , 4: double^#(s(x)) -> c_7(double^#(x)) 880.04/295.40 , 5: double^#(0()) -> c_8() 880.04/295.40 , 6: le^#(s(u), s(v)) -> c_4(le^#(u, v)) 880.04/295.40 , 7: le^#(s(u), 0()) -> c_5() 880.04/295.40 , 8: le^#(0(), v) -> c_6() 880.04/295.40 , 9: square^#(s(x)) -> c_9(plus^#(square(x), double(x))) 880.04/295.40 , 10: square^#(0()) -> c_10() 880.04/295.40 , 11: plus^#(n, s(m)) -> c_11(plus^#(n, m)) 880.04/295.40 , 12: plus^#(n, 0()) -> c_12(n) } 880.04/295.40 880.04/295.40 We are left with following problem, upon which TcT provides the 880.04/295.40 certificate MAYBE. 880.04/295.40 880.04/295.40 Strict DPs: 880.04/295.40 { log^#(x, s(s(y))) -> c_1(cond^#(le(x, s(s(y))), x, y)) 880.04/295.40 , cond^#(false(), x, y) -> c_3(double^#(log(x, square(s(s(y)))))) 880.04/295.40 , double^#(s(x)) -> c_7(double^#(x)) 880.04/295.40 , le^#(s(u), s(v)) -> c_4(le^#(u, v)) 880.04/295.40 , square^#(s(x)) -> c_9(plus^#(square(x), double(x))) 880.04/295.40 , plus^#(n, s(m)) -> c_11(plus^#(n, m)) 880.04/295.40 , plus^#(n, 0()) -> c_12(n) } 880.04/295.40 Strict Trs: 880.04/295.40 { log(x, s(s(y))) -> cond(le(x, s(s(y))), x, y) 880.04/295.40 , cond(true(), x, y) -> s(0()) 880.04/295.40 , cond(false(), x, y) -> double(log(x, square(s(s(y))))) 880.04/295.40 , le(s(u), s(v)) -> le(u, v) 880.04/295.40 , le(s(u), 0()) -> false() 880.04/295.40 , le(0(), v) -> true() 880.04/295.40 , double(s(x)) -> s(s(double(x))) 880.04/295.40 , double(0()) -> 0() 880.04/295.40 , square(s(x)) -> s(plus(square(x), double(x))) 880.04/295.40 , square(0()) -> 0() 880.04/295.40 , plus(n, s(m)) -> s(plus(n, m)) 880.04/295.40 , plus(n, 0()) -> n } 880.04/295.40 Weak DPs: 880.04/295.40 { cond^#(true(), x, y) -> c_2() 880.04/295.40 , double^#(0()) -> c_8() 880.04/295.40 , le^#(s(u), 0()) -> c_5() 880.04/295.40 , le^#(0(), v) -> c_6() 880.04/295.40 , square^#(0()) -> c_10() } 880.04/295.40 Obligation: 880.04/295.40 runtime complexity 880.04/295.40 Answer: 880.04/295.40 MAYBE 880.04/295.40 880.04/295.40 Empty strict component of the problem is NOT empty. 880.04/295.40 880.04/295.40 880.04/295.40 Arrrr.. 880.35/295.78 EOF