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