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