MAYBE 63.55/24.46 MAYBE 63.55/24.46 63.55/24.46 We are left with following problem, upon which TcT provides the 63.55/24.46 certificate MAYBE. 63.55/24.46 63.55/24.46 Strict Trs: 63.55/24.46 { bin(x, 0()) -> s(0()) 63.55/24.46 , bin(0(), s(y)) -> 0() 63.55/24.46 , bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)) } 63.55/24.46 Obligation: 63.55/24.46 runtime complexity 63.55/24.46 Answer: 63.55/24.46 MAYBE 63.55/24.46 63.55/24.46 None of the processors succeeded. 63.55/24.46 63.55/24.46 Details of failed attempt(s): 63.55/24.46 ----------------------------- 63.55/24.46 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 63.55/24.46 following reason: 63.55/24.46 63.55/24.46 We add the following weak dependency pairs: 63.55/24.46 63.55/24.46 Strict DPs: 63.55/24.46 { bin^#(x, 0()) -> c_1() 63.55/24.46 , bin^#(0(), s(y)) -> c_2() 63.55/24.46 , bin^#(s(x), s(y)) -> c_3(bin^#(x, s(y)), bin^#(x, y)) } 63.55/24.46 63.55/24.46 and mark the set of starting terms. 63.55/24.46 63.55/24.46 We are left with following problem, upon which TcT provides the 63.55/24.46 certificate MAYBE. 63.55/24.46 63.55/24.46 Strict DPs: 63.55/24.46 { bin^#(x, 0()) -> c_1() 63.55/24.46 , bin^#(0(), s(y)) -> c_2() 63.55/24.46 , bin^#(s(x), s(y)) -> c_3(bin^#(x, s(y)), bin^#(x, y)) } 63.55/24.46 Strict Trs: 63.55/24.46 { bin(x, 0()) -> s(0()) 63.55/24.46 , bin(0(), s(y)) -> 0() 63.55/24.46 , bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)) } 63.55/24.46 Obligation: 63.55/24.46 runtime complexity 63.55/24.46 Answer: 63.55/24.46 MAYBE 63.55/24.46 63.55/24.46 No rule is usable, rules are removed from the input problem. 63.55/24.46 63.55/24.46 We are left with following problem, upon which TcT provides the 63.55/24.46 certificate MAYBE. 63.55/24.46 63.55/24.46 Strict DPs: 63.55/24.46 { bin^#(x, 0()) -> c_1() 63.55/24.46 , bin^#(0(), s(y)) -> c_2() 63.55/24.46 , bin^#(s(x), s(y)) -> c_3(bin^#(x, s(y)), bin^#(x, y)) } 63.55/24.46 Obligation: 63.55/24.46 runtime complexity 63.55/24.46 Answer: 63.55/24.46 MAYBE 63.55/24.46 63.55/24.46 The weightgap principle applies (using the following constant 63.55/24.46 growth matrix-interpretation) 63.55/24.46 63.55/24.46 The following argument positions are usable: 63.55/24.46 Uargs(c_3) = {1, 2} 63.55/24.46 63.55/24.46 TcT has computed the following constructor-restricted matrix 63.55/24.46 interpretation. 63.55/24.46 63.55/24.46 [0] = [0] 63.55/24.46 [0] 63.55/24.46 63.55/24.46 [s](x1) = [1 1] x1 + [0] 63.55/24.46 [0 1] [0] 63.55/24.46 63.55/24.46 [bin^#](x1, x2) = [1] 63.55/24.47 [0] 63.55/24.47 63.55/24.47 [c_1] = [0] 63.55/24.47 [0] 63.55/24.47 63.55/24.47 [c_2] = [0] 63.55/24.47 [0] 63.55/24.47 63.55/24.47 [c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 63.55/24.47 [0 1] [0 1] [2] 63.55/24.47 63.55/24.47 The order satisfies the following ordering constraints: 63.55/24.47 63.55/24.47 [bin^#(x, 0())] = [1] 63.55/24.47 [0] 63.55/24.47 > [0] 63.55/24.47 [0] 63.55/24.47 = [c_1()] 63.55/24.47 63.55/24.47 [bin^#(0(), s(y))] = [1] 63.55/24.47 [0] 63.55/24.47 > [0] 63.55/24.47 [0] 63.55/24.47 = [c_2()] 63.55/24.47 63.55/24.47 [bin^#(s(x), s(y))] = [1] 63.55/24.47 [0] 63.55/24.47 ? [3] 63.55/24.47 [2] 63.55/24.47 = [c_3(bin^#(x, s(y)), bin^#(x, y))] 63.55/24.47 63.55/24.47 63.55/24.47 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 63.55/24.47 63.55/24.47 We are left with following problem, upon which TcT provides the 63.55/24.47 certificate MAYBE. 63.55/24.47 63.55/24.47 Strict DPs: 63.55/24.47 { bin^#(s(x), s(y)) -> c_3(bin^#(x, s(y)), bin^#(x, y)) } 63.55/24.47 Weak DPs: 63.55/24.47 { bin^#(x, 0()) -> c_1() 63.55/24.47 , bin^#(0(), s(y)) -> c_2() } 63.55/24.47 Obligation: 63.55/24.47 runtime complexity 63.55/24.47 Answer: 63.55/24.47 MAYBE 63.55/24.47 63.55/24.47 The following weak DPs constitute a sub-graph of the DG that is 63.55/24.47 closed under successors. The DPs are removed. 63.55/24.47 63.55/24.47 { bin^#(x, 0()) -> c_1() 63.55/24.47 , bin^#(0(), s(y)) -> c_2() } 63.55/24.47 63.55/24.47 We are left with following problem, upon which TcT provides the 63.55/24.47 certificate MAYBE. 63.55/24.47 63.55/24.47 Strict DPs: 63.55/24.47 { bin^#(s(x), s(y)) -> c_3(bin^#(x, s(y)), bin^#(x, y)) } 63.55/24.47 Obligation: 63.55/24.47 runtime complexity 63.55/24.47 Answer: 63.55/24.47 MAYBE 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'empty' failed due to the following reason: 63.55/24.47 63.55/24.47 Empty strict component of the problem is NOT empty. 63.55/24.47 63.55/24.47 2) 'Inspecting Problem...' failed due to the following reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'empty' failed due to the following reason: 63.55/24.47 63.55/24.47 Empty strict component of the problem is NOT empty. 63.55/24.47 63.55/24.47 2) 'Fastest' failed due to the following reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'With Problem ...' failed due to the following reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'empty' failed due to the following reason: 63.55/24.47 63.55/24.47 Empty strict component of the problem is NOT empty. 63.55/24.47 63.55/24.47 2) 'Polynomial Path Order (PS)' failed due to the following reason: 63.55/24.47 63.55/24.47 The processor is inapplicable, reason: 63.55/24.47 Processor only applicable for innermost runtime complexity analysis 63.55/24.47 63.55/24.47 63.55/24.47 2) 'Fastest (timeout of 24 seconds)' failed due to the following 63.55/24.47 reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 63.55/24.47 failed due to the following reason: 63.55/24.47 63.55/24.47 match-boundness of the problem could not be verified. 63.55/24.47 63.55/24.47 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 63.55/24.47 failed due to the following reason: 63.55/24.47 63.55/24.47 match-boundness of the problem could not be verified. 63.55/24.47 63.55/24.47 63.55/24.47 3) 'Polynomial Path Order (PS)' failed due to the following reason: 63.55/24.47 63.55/24.47 The processor is inapplicable, reason: 63.55/24.47 Processor only applicable for innermost runtime complexity analysis 63.55/24.47 63.55/24.47 63.55/24.47 63.55/24.47 63.55/24.47 2) 'Best' failed due to the following reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 63.55/24.47 seconds)' failed due to the following reason: 63.55/24.47 63.55/24.47 The weightgap principle applies (using the following nonconstant 63.55/24.47 growth matrix-interpretation) 63.55/24.47 63.55/24.47 The following argument positions are usable: 63.55/24.47 Uargs(+) = {1, 2} 63.55/24.47 63.55/24.47 TcT has computed the following matrix interpretation satisfying 63.55/24.47 not(EDA) and not(IDA(1)). 63.55/24.47 63.55/24.47 [bin](x1, x2) = [3] 63.55/24.47 63.55/24.47 [0] = [2] 63.55/24.47 63.55/24.47 [s](x1) = [1] x1 + [4] 63.55/24.47 63.55/24.47 [+](x1, x2) = [1] x1 + [1] x2 + [7] 63.55/24.47 63.55/24.47 The order satisfies the following ordering constraints: 63.55/24.47 63.55/24.47 [bin(x, 0())] = [3] 63.55/24.47 ? [6] 63.55/24.47 = [s(0())] 63.55/24.47 63.55/24.47 [bin(0(), s(y))] = [3] 63.55/24.47 > [2] 63.55/24.47 = [0()] 63.55/24.47 63.55/24.47 [bin(s(x), s(y))] = [3] 63.55/24.47 ? [13] 63.55/24.47 = [+(bin(x, s(y)), bin(x, y))] 63.55/24.47 63.55/24.47 63.55/24.47 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 63.55/24.47 63.55/24.47 We are left with following problem, upon which TcT provides the 63.55/24.47 certificate MAYBE. 63.55/24.47 63.55/24.47 Strict Trs: 63.55/24.47 { bin(x, 0()) -> s(0()) 63.55/24.47 , bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)) } 63.55/24.47 Weak Trs: { bin(0(), s(y)) -> 0() } 63.55/24.47 Obligation: 63.55/24.47 runtime complexity 63.55/24.47 Answer: 63.55/24.47 MAYBE 63.55/24.47 63.55/24.47 The weightgap principle applies (using the following nonconstant 63.55/24.47 growth matrix-interpretation) 63.55/24.47 63.55/24.47 The following argument positions are usable: 63.55/24.47 Uargs(+) = {1, 2} 63.55/24.47 63.55/24.47 TcT has computed the following matrix interpretation satisfying 63.55/24.47 not(EDA) and not(IDA(1)). 63.55/24.47 63.55/24.47 [bin](x1, x2) = [3] 63.55/24.47 63.55/24.47 [0] = [2] 63.55/24.47 63.55/24.47 [s](x1) = [1] x1 + [0] 63.55/24.47 63.55/24.47 [+](x1, x2) = [1] x1 + [1] x2 + [7] 63.55/24.47 63.55/24.47 The order satisfies the following ordering constraints: 63.55/24.47 63.55/24.47 [bin(x, 0())] = [3] 63.55/24.47 > [2] 63.55/24.47 = [s(0())] 63.55/24.47 63.55/24.47 [bin(0(), s(y))] = [3] 63.55/24.47 > [2] 63.55/24.47 = [0()] 63.55/24.47 63.55/24.47 [bin(s(x), s(y))] = [3] 63.55/24.47 ? [13] 63.55/24.47 = [+(bin(x, s(y)), bin(x, y))] 63.55/24.47 63.55/24.47 63.55/24.47 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 63.55/24.47 63.55/24.47 We are left with following problem, upon which TcT provides the 63.55/24.47 certificate MAYBE. 63.55/24.47 63.55/24.47 Strict Trs: { bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)) } 63.55/24.47 Weak Trs: 63.55/24.47 { bin(x, 0()) -> s(0()) 63.55/24.47 , bin(0(), s(y)) -> 0() } 63.55/24.47 Obligation: 63.55/24.47 runtime complexity 63.55/24.47 Answer: 63.55/24.47 MAYBE 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'empty' failed due to the following reason: 63.55/24.47 63.55/24.47 Empty strict component of the problem is NOT empty. 63.55/24.47 63.55/24.47 2) 'With Problem ...' failed due to the following reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'empty' failed due to the following reason: 63.55/24.47 63.55/24.47 Empty strict component of the problem is NOT empty. 63.55/24.47 63.55/24.47 2) 'Fastest' failed due to the following reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'With Problem ...' failed due to the following reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'empty' failed due to the following reason: 63.55/24.47 63.55/24.47 Empty strict component of the problem is NOT empty. 63.55/24.47 63.55/24.47 2) 'With Problem ...' failed due to the following reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'empty' failed due to the following reason: 63.55/24.47 63.55/24.47 Empty strict component of the problem is NOT empty. 63.55/24.47 63.55/24.47 2) 'With Problem ...' failed due to the following reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'empty' failed due to the following reason: 63.55/24.47 63.55/24.47 Empty strict component of the problem is NOT empty. 63.55/24.47 63.55/24.47 2) 'With Problem ...' failed due to the following reason: 63.55/24.47 63.55/24.47 Empty strict component of the problem is NOT empty. 63.55/24.47 63.55/24.47 63.55/24.47 63.55/24.47 63.55/24.47 2) 'With Problem ...' failed due to the following reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'empty' failed due to the following reason: 63.55/24.47 63.55/24.47 Empty strict component of the problem is NOT empty. 63.55/24.47 63.55/24.47 2) 'With Problem ...' failed due to the following reason: 63.55/24.47 63.55/24.47 Empty strict component of the problem is NOT empty. 63.55/24.47 63.55/24.47 63.55/24.47 63.55/24.47 63.55/24.47 63.55/24.47 2) 'Best' failed due to the following reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 63.55/24.47 to the following reason: 63.55/24.47 63.55/24.47 The processor is inapplicable, reason: 63.55/24.47 Processor only applicable for innermost runtime complexity analysis 63.55/24.47 63.55/24.47 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 63.55/24.47 following reason: 63.55/24.47 63.55/24.47 The processor is inapplicable, reason: 63.55/24.47 Processor only applicable for innermost runtime complexity analysis 63.55/24.47 63.55/24.47 63.55/24.47 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 63.55/24.47 failed due to the following reason: 63.55/24.47 63.55/24.47 None of the processors succeeded. 63.55/24.47 63.55/24.47 Details of failed attempt(s): 63.55/24.47 ----------------------------- 63.55/24.47 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 63.55/24.47 failed due to the following reason: 63.55/24.47 63.55/24.47 match-boundness of the problem could not be verified. 63.55/24.47 63.55/24.47 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 63.55/24.47 failed due to the following reason: 63.55/24.47 63.55/24.47 match-boundness of the problem could not be verified. 63.55/24.47 63.55/24.47 63.55/24.47 63.55/24.47 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 63.55/24.47 the following reason: 63.55/24.47 63.55/24.47 We add the following weak dependency pairs: 63.55/24.47 63.55/24.47 Strict DPs: 63.55/24.47 { bin^#(x, 0()) -> c_1() 63.55/24.47 , bin^#(0(), s(y)) -> c_2() 63.55/24.47 , bin^#(s(x), s(y)) -> c_3(bin^#(x, s(y)), bin^#(x, y)) } 63.55/24.47 63.55/24.47 and mark the set of starting terms. 63.55/24.47 63.55/24.47 We are left with following problem, upon which TcT provides the 63.55/24.47 certificate MAYBE. 63.55/24.47 63.55/24.47 Strict DPs: 63.55/24.47 { bin^#(x, 0()) -> c_1() 63.55/24.47 , bin^#(0(), s(y)) -> c_2() 63.55/24.47 , bin^#(s(x), s(y)) -> c_3(bin^#(x, s(y)), bin^#(x, y)) } 63.55/24.47 Strict Trs: 63.55/24.47 { bin(x, 0()) -> s(0()) 63.55/24.47 , bin(0(), s(y)) -> 0() 63.55/24.47 , bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)) } 63.55/24.47 Obligation: 63.55/24.47 runtime complexity 63.55/24.47 Answer: 63.55/24.47 MAYBE 63.55/24.47 63.55/24.47 We estimate the number of application of {1,2} by applications of 63.55/24.47 Pre({1,2}) = {3}. Here rules are labeled as follows: 63.55/24.47 63.55/24.47 DPs: 63.55/24.47 { 1: bin^#(x, 0()) -> c_1() 63.55/24.47 , 2: bin^#(0(), s(y)) -> c_2() 63.55/24.47 , 3: bin^#(s(x), s(y)) -> c_3(bin^#(x, s(y)), bin^#(x, y)) } 63.55/24.47 63.55/24.47 We are left with following problem, upon which TcT provides the 63.55/24.47 certificate MAYBE. 63.55/24.47 63.55/24.47 Strict DPs: 63.55/24.47 { bin^#(s(x), s(y)) -> c_3(bin^#(x, s(y)), bin^#(x, y)) } 63.55/24.47 Strict Trs: 63.55/24.47 { bin(x, 0()) -> s(0()) 63.55/24.47 , bin(0(), s(y)) -> 0() 63.55/24.47 , bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)) } 63.55/24.47 Weak DPs: 63.55/24.47 { bin^#(x, 0()) -> c_1() 63.55/24.47 , bin^#(0(), s(y)) -> c_2() } 63.55/24.47 Obligation: 63.55/24.47 runtime complexity 63.55/24.47 Answer: 63.55/24.47 MAYBE 63.55/24.47 63.55/24.47 Empty strict component of the problem is NOT empty. 63.55/24.47 63.55/24.47 63.55/24.47 Arrrr.. 63.86/24.51 EOF