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