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