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