MAYBE 697.86/297.03 MAYBE 697.86/297.03 697.86/297.03 We are left with following problem, upon which TcT provides the 697.86/297.03 certificate MAYBE. 697.86/297.03 697.86/297.03 Strict Trs: 697.86/297.03 { fact(X) -> 697.86/297.03 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 697.86/297.03 , fact(X) -> n__fact(X) 697.86/297.03 , if(true(), X, Y) -> activate(X) 697.86/297.03 , if(false(), X, Y) -> activate(Y) 697.86/297.03 , zero(0()) -> true() 697.86/297.03 , zero(s(X)) -> false() 697.86/297.03 , add(0(), X) -> X 697.86/297.03 , add(s(X), Y) -> s(add(X, Y)) 697.86/297.03 , 0() -> n__0() 697.86/297.03 , s(X) -> n__s(X) 697.86/297.03 , prod(X1, X2) -> n__prod(X1, X2) 697.86/297.03 , prod(0(), X) -> 0() 697.86/297.03 , prod(s(X), Y) -> add(Y, prod(X, Y)) 697.86/297.03 , activate(X) -> X 697.86/297.03 , activate(n__s(X)) -> s(activate(X)) 697.86/297.03 , activate(n__0()) -> 0() 697.86/297.03 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 697.86/297.03 , activate(n__fact(X)) -> fact(activate(X)) 697.86/297.03 , activate(n__p(X)) -> p(activate(X)) 697.86/297.03 , p(X) -> n__p(X) 697.86/297.03 , p(s(X)) -> X } 697.86/297.03 Obligation: 697.86/297.03 runtime complexity 697.86/297.03 Answer: 697.86/297.03 MAYBE 697.86/297.03 697.86/297.03 None of the processors succeeded. 697.86/297.03 697.86/297.03 Details of failed attempt(s): 697.86/297.03 ----------------------------- 697.86/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 697.86/297.03 following reason: 697.86/297.03 697.86/297.03 Computation stopped due to timeout after 297.0 seconds. 697.86/297.03 697.86/297.03 2) 'Best' failed due to the following reason: 697.86/297.03 697.86/297.03 None of the processors succeeded. 697.86/297.03 697.86/297.03 Details of failed attempt(s): 697.86/297.03 ----------------------------- 697.86/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 697.86/297.03 seconds)' failed due to the following reason: 697.86/297.03 697.86/297.03 None of the processors succeeded. 697.86/297.03 697.86/297.03 Details of failed attempt(s): 697.86/297.03 ----------------------------- 697.86/297.03 1) 'empty' failed due to the following reason: 697.86/297.03 697.86/297.03 Empty strict component of the problem is NOT empty. 697.86/297.03 697.86/297.03 2) 'With Problem ...' failed due to the following reason: 697.86/297.03 697.86/297.03 None of the processors succeeded. 697.86/297.03 697.86/297.03 Details of failed attempt(s): 697.86/297.03 ----------------------------- 697.86/297.03 1) 'empty' failed due to the following reason: 697.86/297.03 697.86/297.03 Empty strict component of the problem is NOT empty. 697.86/297.03 697.86/297.03 2) 'Fastest' failed due to the following reason: 697.86/297.03 697.86/297.03 None of the processors succeeded. 697.86/297.03 697.86/297.03 Details of failed attempt(s): 697.86/297.03 ----------------------------- 697.86/297.03 1) 'With Problem ...' failed due to the following reason: 697.86/297.03 697.86/297.03 None of the processors succeeded. 697.86/297.03 697.86/297.03 Details of failed attempt(s): 697.86/297.03 ----------------------------- 697.86/297.03 1) 'empty' failed due to the following reason: 697.86/297.03 697.86/297.03 Empty strict component of the problem is NOT empty. 697.86/297.03 697.86/297.03 2) 'With Problem ...' failed due to the following reason: 697.86/297.03 697.86/297.03 None of the processors succeeded. 697.86/297.03 697.86/297.03 Details of failed attempt(s): 697.86/297.03 ----------------------------- 697.86/297.03 1) 'empty' failed due to the following reason: 697.86/297.03 697.86/297.03 Empty strict component of the problem is NOT empty. 697.86/297.03 697.86/297.03 2) 'With Problem ...' failed due to the following reason: 697.86/297.03 697.86/297.03 None of the processors succeeded. 697.86/297.03 697.86/297.03 Details of failed attempt(s): 697.86/297.03 ----------------------------- 697.86/297.03 1) 'empty' failed due to the following reason: 697.86/297.03 697.86/297.03 Empty strict component of the problem is NOT empty. 697.86/297.03 697.86/297.03 2) 'With Problem ...' failed due to the following reason: 697.86/297.03 697.86/297.03 Empty strict component of the problem is NOT empty. 697.86/297.03 697.86/297.03 697.86/297.03 697.86/297.03 697.86/297.03 2) 'With Problem ...' failed due to the following reason: 697.86/297.03 697.86/297.03 None of the processors succeeded. 697.86/297.03 697.86/297.03 Details of failed attempt(s): 697.86/297.03 ----------------------------- 697.86/297.03 1) 'empty' failed due to the following reason: 697.86/297.03 697.86/297.03 Empty strict component of the problem is NOT empty. 697.86/297.03 697.86/297.03 2) 'With Problem ...' failed due to the following reason: 697.86/297.03 697.86/297.03 Empty strict component of the problem is NOT empty. 697.86/297.03 697.86/297.03 697.86/297.03 697.86/297.03 697.86/297.03 697.86/297.03 2) 'Best' failed due to the following reason: 697.86/297.03 697.86/297.03 None of the processors succeeded. 697.86/297.03 697.86/297.03 Details of failed attempt(s): 697.86/297.03 ----------------------------- 697.86/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 697.86/297.03 following reason: 697.86/297.03 697.86/297.03 The processor is inapplicable, reason: 697.86/297.03 Processor only applicable for innermost runtime complexity analysis 697.86/297.03 697.86/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 697.86/297.03 to the following reason: 697.86/297.03 697.86/297.03 The processor is inapplicable, reason: 697.86/297.03 Processor only applicable for innermost runtime complexity analysis 697.86/297.03 697.86/297.03 697.86/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 697.86/297.03 failed due to the following reason: 697.86/297.03 697.86/297.03 None of the processors succeeded. 697.86/297.03 697.86/297.03 Details of failed attempt(s): 697.86/297.03 ----------------------------- 697.86/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 697.86/297.03 failed due to the following reason: 697.86/297.03 697.86/297.03 match-boundness of the problem could not be verified. 697.86/297.03 697.86/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 697.86/297.03 failed due to the following reason: 697.86/297.03 697.86/297.03 match-boundness of the problem could not be verified. 697.86/297.03 697.86/297.03 697.86/297.03 697.86/297.03 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 697.86/297.03 the following reason: 697.86/297.03 697.86/297.03 We add the following weak dependency pairs: 697.86/297.03 697.86/297.03 Strict DPs: 697.86/297.03 { fact^#(X) -> 697.86/297.03 c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))) 697.86/297.03 , fact^#(X) -> c_2(X) 697.86/297.03 , if^#(true(), X, Y) -> c_3(activate^#(X)) 697.86/297.03 , if^#(false(), X, Y) -> c_4(activate^#(Y)) 697.86/297.03 , activate^#(X) -> c_14(X) 697.86/297.03 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 697.86/297.03 , activate^#(n__0()) -> c_16(0^#()) 697.86/297.03 , activate^#(n__prod(X1, X2)) -> 697.86/297.03 c_17(prod^#(activate(X1), activate(X2))) 697.86/297.03 , activate^#(n__fact(X)) -> c_18(fact^#(activate(X))) 697.86/297.03 , activate^#(n__p(X)) -> c_19(p^#(activate(X))) 697.86/297.03 , zero^#(0()) -> c_5() 697.86/297.03 , zero^#(s(X)) -> c_6() 697.86/297.03 , add^#(0(), X) -> c_7(X) 697.86/297.03 , add^#(s(X), Y) -> c_8(s^#(add(X, Y))) 697.86/297.03 , s^#(X) -> c_10(X) 697.86/297.03 , 0^#() -> c_9() 697.86/297.03 , prod^#(X1, X2) -> c_11(X1, X2) 697.86/297.03 , prod^#(0(), X) -> c_12(0^#()) 697.86/297.03 , prod^#(s(X), Y) -> c_13(add^#(Y, prod(X, Y))) 697.86/297.03 , p^#(X) -> c_20(X) 697.86/297.03 , p^#(s(X)) -> c_21(X) } 697.86/297.03 697.86/297.03 and mark the set of starting terms. 697.86/297.03 697.86/297.03 We are left with following problem, upon which TcT provides the 697.86/297.03 certificate MAYBE. 697.86/297.03 697.86/297.03 Strict DPs: 697.86/297.03 { fact^#(X) -> 697.86/297.03 c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))) 697.86/297.03 , fact^#(X) -> c_2(X) 697.86/297.03 , if^#(true(), X, Y) -> c_3(activate^#(X)) 697.86/297.03 , if^#(false(), X, Y) -> c_4(activate^#(Y)) 697.86/297.03 , activate^#(X) -> c_14(X) 697.86/297.03 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 697.86/297.03 , activate^#(n__0()) -> c_16(0^#()) 697.86/297.03 , activate^#(n__prod(X1, X2)) -> 697.86/297.03 c_17(prod^#(activate(X1), activate(X2))) 697.86/297.03 , activate^#(n__fact(X)) -> c_18(fact^#(activate(X))) 697.86/297.03 , activate^#(n__p(X)) -> c_19(p^#(activate(X))) 697.86/297.03 , zero^#(0()) -> c_5() 697.86/297.03 , zero^#(s(X)) -> c_6() 697.86/297.03 , add^#(0(), X) -> c_7(X) 697.86/297.03 , add^#(s(X), Y) -> c_8(s^#(add(X, Y))) 697.86/297.03 , s^#(X) -> c_10(X) 697.86/297.03 , 0^#() -> c_9() 697.86/297.03 , prod^#(X1, X2) -> c_11(X1, X2) 697.86/297.03 , prod^#(0(), X) -> c_12(0^#()) 697.86/297.03 , prod^#(s(X), Y) -> c_13(add^#(Y, prod(X, Y))) 697.86/297.03 , p^#(X) -> c_20(X) 697.86/297.03 , p^#(s(X)) -> c_21(X) } 697.86/297.03 Strict Trs: 697.86/297.03 { fact(X) -> 697.86/297.03 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 697.86/297.03 , fact(X) -> n__fact(X) 697.86/297.03 , if(true(), X, Y) -> activate(X) 697.86/297.03 , if(false(), X, Y) -> activate(Y) 697.86/297.03 , zero(0()) -> true() 697.86/297.03 , zero(s(X)) -> false() 697.86/297.03 , add(0(), X) -> X 697.86/297.03 , add(s(X), Y) -> s(add(X, Y)) 697.86/297.03 , 0() -> n__0() 697.86/297.03 , s(X) -> n__s(X) 697.86/297.03 , prod(X1, X2) -> n__prod(X1, X2) 697.86/297.03 , prod(0(), X) -> 0() 697.86/297.03 , prod(s(X), Y) -> add(Y, prod(X, Y)) 697.86/297.03 , activate(X) -> X 697.86/297.03 , activate(n__s(X)) -> s(activate(X)) 697.86/297.03 , activate(n__0()) -> 0() 697.86/297.03 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 697.86/297.03 , activate(n__fact(X)) -> fact(activate(X)) 697.86/297.03 , activate(n__p(X)) -> p(activate(X)) 697.86/297.03 , p(X) -> n__p(X) 697.86/297.03 , p(s(X)) -> X } 697.86/297.03 Obligation: 697.86/297.03 runtime complexity 697.86/297.03 Answer: 697.86/297.03 MAYBE 697.86/297.03 697.86/297.03 We estimate the number of application of {11,12,16} by applications 697.86/297.03 of Pre({11,12,16}) = {2,5,7,13,15,17,18,20,21}. Here rules are 697.86/297.03 labeled as follows: 697.86/297.03 697.86/297.03 DPs: 697.86/297.03 { 1: fact^#(X) -> 697.86/297.03 c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))) 697.86/297.03 , 2: fact^#(X) -> c_2(X) 697.86/297.03 , 3: if^#(true(), X, Y) -> c_3(activate^#(X)) 697.86/297.03 , 4: if^#(false(), X, Y) -> c_4(activate^#(Y)) 697.86/297.03 , 5: activate^#(X) -> c_14(X) 697.86/297.03 , 6: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 697.86/297.03 , 7: activate^#(n__0()) -> c_16(0^#()) 697.86/297.03 , 8: activate^#(n__prod(X1, X2)) -> 697.86/297.03 c_17(prod^#(activate(X1), activate(X2))) 697.86/297.03 , 9: activate^#(n__fact(X)) -> c_18(fact^#(activate(X))) 697.86/297.03 , 10: activate^#(n__p(X)) -> c_19(p^#(activate(X))) 697.86/297.03 , 11: zero^#(0()) -> c_5() 697.86/297.03 , 12: zero^#(s(X)) -> c_6() 697.86/297.03 , 13: add^#(0(), X) -> c_7(X) 697.86/297.03 , 14: add^#(s(X), Y) -> c_8(s^#(add(X, Y))) 697.86/297.03 , 15: s^#(X) -> c_10(X) 697.86/297.03 , 16: 0^#() -> c_9() 697.86/297.03 , 17: prod^#(X1, X2) -> c_11(X1, X2) 697.86/297.03 , 18: prod^#(0(), X) -> c_12(0^#()) 697.86/297.03 , 19: prod^#(s(X), Y) -> c_13(add^#(Y, prod(X, Y))) 697.86/297.03 , 20: p^#(X) -> c_20(X) 697.86/297.03 , 21: p^#(s(X)) -> c_21(X) } 697.86/297.03 697.86/297.03 We are left with following problem, upon which TcT provides the 697.86/297.03 certificate MAYBE. 697.86/297.03 697.86/297.03 Strict DPs: 697.86/297.03 { fact^#(X) -> 697.86/297.03 c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))) 697.86/297.03 , fact^#(X) -> c_2(X) 697.86/297.03 , if^#(true(), X, Y) -> c_3(activate^#(X)) 697.86/297.03 , if^#(false(), X, Y) -> c_4(activate^#(Y)) 697.86/297.03 , activate^#(X) -> c_14(X) 697.86/297.03 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 697.86/297.03 , activate^#(n__0()) -> c_16(0^#()) 697.86/297.03 , activate^#(n__prod(X1, X2)) -> 697.86/297.03 c_17(prod^#(activate(X1), activate(X2))) 697.86/297.03 , activate^#(n__fact(X)) -> c_18(fact^#(activate(X))) 697.86/297.03 , activate^#(n__p(X)) -> c_19(p^#(activate(X))) 697.86/297.03 , add^#(0(), X) -> c_7(X) 697.86/297.03 , add^#(s(X), Y) -> c_8(s^#(add(X, Y))) 697.86/297.03 , s^#(X) -> c_10(X) 697.86/297.03 , prod^#(X1, X2) -> c_11(X1, X2) 697.86/297.03 , prod^#(0(), X) -> c_12(0^#()) 697.86/297.03 , prod^#(s(X), Y) -> c_13(add^#(Y, prod(X, Y))) 697.86/297.03 , p^#(X) -> c_20(X) 697.86/297.03 , p^#(s(X)) -> c_21(X) } 697.86/297.03 Strict Trs: 697.86/297.03 { fact(X) -> 697.86/297.03 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 697.86/297.03 , fact(X) -> n__fact(X) 697.86/297.03 , if(true(), X, Y) -> activate(X) 697.86/297.03 , if(false(), X, Y) -> activate(Y) 697.86/297.03 , zero(0()) -> true() 697.86/297.03 , zero(s(X)) -> false() 697.86/297.03 , add(0(), X) -> X 697.86/297.03 , add(s(X), Y) -> s(add(X, Y)) 697.86/297.03 , 0() -> n__0() 697.86/297.03 , s(X) -> n__s(X) 697.86/297.03 , prod(X1, X2) -> n__prod(X1, X2) 697.86/297.03 , prod(0(), X) -> 0() 697.86/297.03 , prod(s(X), Y) -> add(Y, prod(X, Y)) 697.86/297.03 , activate(X) -> X 697.86/297.03 , activate(n__s(X)) -> s(activate(X)) 697.86/297.03 , activate(n__0()) -> 0() 697.86/297.03 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 697.86/297.03 , activate(n__fact(X)) -> fact(activate(X)) 697.86/297.03 , activate(n__p(X)) -> p(activate(X)) 697.86/297.03 , p(X) -> n__p(X) 697.86/297.03 , p(s(X)) -> X } 697.86/297.03 Weak DPs: 697.86/297.03 { zero^#(0()) -> c_5() 697.86/297.03 , zero^#(s(X)) -> c_6() 697.86/297.03 , 0^#() -> c_9() } 697.86/297.03 Obligation: 697.86/297.03 runtime complexity 697.86/297.03 Answer: 697.86/297.03 MAYBE 697.86/297.03 697.86/297.03 We estimate the number of application of {7,15} by applications of 697.86/297.03 Pre({7,15}) = {2,3,4,5,8,11,13,14,17,18}. Here rules are labeled as 697.86/297.03 follows: 697.86/297.03 697.86/297.03 DPs: 697.86/297.03 { 1: fact^#(X) -> 697.86/297.03 c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))) 697.86/297.03 , 2: fact^#(X) -> c_2(X) 697.86/297.03 , 3: if^#(true(), X, Y) -> c_3(activate^#(X)) 697.86/297.03 , 4: if^#(false(), X, Y) -> c_4(activate^#(Y)) 697.86/297.03 , 5: activate^#(X) -> c_14(X) 697.86/297.03 , 6: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 697.86/297.03 , 7: activate^#(n__0()) -> c_16(0^#()) 697.86/297.03 , 8: activate^#(n__prod(X1, X2)) -> 697.86/297.03 c_17(prod^#(activate(X1), activate(X2))) 697.86/297.03 , 9: activate^#(n__fact(X)) -> c_18(fact^#(activate(X))) 697.86/297.03 , 10: activate^#(n__p(X)) -> c_19(p^#(activate(X))) 697.86/297.03 , 11: add^#(0(), X) -> c_7(X) 697.86/297.03 , 12: add^#(s(X), Y) -> c_8(s^#(add(X, Y))) 697.86/297.03 , 13: s^#(X) -> c_10(X) 697.86/297.03 , 14: prod^#(X1, X2) -> c_11(X1, X2) 697.86/297.03 , 15: prod^#(0(), X) -> c_12(0^#()) 697.86/297.03 , 16: prod^#(s(X), Y) -> c_13(add^#(Y, prod(X, Y))) 697.86/297.03 , 17: p^#(X) -> c_20(X) 697.86/297.03 , 18: p^#(s(X)) -> c_21(X) 697.86/297.03 , 19: zero^#(0()) -> c_5() 697.86/297.03 , 20: zero^#(s(X)) -> c_6() 697.86/297.03 , 21: 0^#() -> c_9() } 697.86/297.03 697.86/297.03 We are left with following problem, upon which TcT provides the 697.86/297.03 certificate MAYBE. 697.86/297.03 697.86/297.03 Strict DPs: 697.86/297.03 { fact^#(X) -> 697.86/297.03 c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))) 697.86/297.03 , fact^#(X) -> c_2(X) 697.86/297.03 , if^#(true(), X, Y) -> c_3(activate^#(X)) 697.86/297.03 , if^#(false(), X, Y) -> c_4(activate^#(Y)) 697.86/297.03 , activate^#(X) -> c_14(X) 697.86/297.03 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 697.86/297.03 , activate^#(n__prod(X1, X2)) -> 697.86/297.03 c_17(prod^#(activate(X1), activate(X2))) 697.86/297.03 , activate^#(n__fact(X)) -> c_18(fact^#(activate(X))) 697.86/297.03 , activate^#(n__p(X)) -> c_19(p^#(activate(X))) 697.86/297.03 , add^#(0(), X) -> c_7(X) 697.86/297.03 , add^#(s(X), Y) -> c_8(s^#(add(X, Y))) 697.86/297.03 , s^#(X) -> c_10(X) 697.86/297.03 , prod^#(X1, X2) -> c_11(X1, X2) 697.86/297.03 , prod^#(s(X), Y) -> c_13(add^#(Y, prod(X, Y))) 697.86/297.03 , p^#(X) -> c_20(X) 697.86/297.03 , p^#(s(X)) -> c_21(X) } 697.86/297.03 Strict Trs: 697.86/297.03 { fact(X) -> 697.86/297.03 if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))) 697.86/297.03 , fact(X) -> n__fact(X) 697.86/297.03 , if(true(), X, Y) -> activate(X) 697.86/297.03 , if(false(), X, Y) -> activate(Y) 697.86/297.03 , zero(0()) -> true() 697.86/297.03 , zero(s(X)) -> false() 697.86/297.03 , add(0(), X) -> X 697.86/297.03 , add(s(X), Y) -> s(add(X, Y)) 697.86/297.03 , 0() -> n__0() 697.86/297.03 , s(X) -> n__s(X) 697.86/297.03 , prod(X1, X2) -> n__prod(X1, X2) 697.86/297.03 , prod(0(), X) -> 0() 697.86/297.03 , prod(s(X), Y) -> add(Y, prod(X, Y)) 697.86/297.03 , activate(X) -> X 697.86/297.03 , activate(n__s(X)) -> s(activate(X)) 697.86/297.03 , activate(n__0()) -> 0() 697.86/297.03 , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2)) 697.86/297.03 , activate(n__fact(X)) -> fact(activate(X)) 697.86/297.03 , activate(n__p(X)) -> p(activate(X)) 697.86/297.03 , p(X) -> n__p(X) 697.86/297.03 , p(s(X)) -> X } 697.86/297.03 Weak DPs: 697.86/297.03 { activate^#(n__0()) -> c_16(0^#()) 697.86/297.03 , zero^#(0()) -> c_5() 697.86/297.03 , zero^#(s(X)) -> c_6() 697.86/297.03 , 0^#() -> c_9() 697.86/297.03 , prod^#(0(), X) -> c_12(0^#()) } 697.86/297.03 Obligation: 697.86/297.03 runtime complexity 697.86/297.03 Answer: 697.86/297.03 MAYBE 697.86/297.03 697.86/297.03 Empty strict component of the problem is NOT empty. 697.86/297.03 697.86/297.03 697.86/297.03 Arrrr.. 698.08/297.20 EOF