MAYBE 171.44/89.09 MAYBE 171.44/89.09 171.44/89.09 We are left with following problem, upon which TcT provides the 171.44/89.09 certificate MAYBE. 171.44/89.09 171.44/89.09 Strict Trs: 171.44/89.09 { lt(x, 0()) -> false() 171.44/89.09 , lt(0(), s(x)) -> true() 171.44/89.09 , lt(s(x), s(y)) -> lt(x, y) 171.44/89.09 , fac(x) -> help(x, 0()) 171.44/89.09 , help(x, c) -> if(lt(c, x), x, c) 171.44/89.09 , if(true(), x, c) -> times(s(c), help(x, s(c))) 171.44/89.09 , if(false(), x, c) -> s(0()) } 171.44/89.09 Obligation: 171.44/89.09 runtime complexity 171.44/89.09 Answer: 171.44/89.09 MAYBE 171.44/89.09 171.44/89.09 None of the processors succeeded. 171.44/89.09 171.44/89.09 Details of failed attempt(s): 171.44/89.09 ----------------------------- 171.44/89.09 1) 'Best' failed due to the following reason: 171.44/89.09 171.44/89.09 None of the processors succeeded. 171.44/89.09 171.44/89.09 Details of failed attempt(s): 171.44/89.09 ----------------------------- 171.44/89.09 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 171.44/89.09 seconds)' failed due to the following reason: 171.44/89.09 171.44/89.09 The weightgap principle applies (using the following nonconstant 171.44/89.09 growth matrix-interpretation) 171.44/89.09 171.44/89.09 The following argument positions are usable: 171.44/89.09 Uargs(if) = {1}, Uargs(times) = {2} 171.44/89.09 171.44/89.09 TcT has computed the following matrix interpretation satisfying 171.44/89.09 not(EDA) and not(IDA(1)). 171.44/89.09 171.44/89.09 [lt](x1, x2) = [4] 171.44/89.09 171.44/89.09 [0] = [7] 171.44/89.09 171.44/89.09 [s](x1) = [0] 171.44/89.09 171.44/89.09 [true] = [1] 171.44/89.09 171.44/89.09 [false] = [1] 171.44/89.09 171.44/89.09 [fac](x1) = [1] x1 + [7] 171.44/89.09 171.44/89.09 [help](x1, x2) = [0] 171.44/89.09 171.44/89.09 [if](x1, x2, x3) = [1] x1 + [0] 171.44/89.09 171.44/89.09 [times](x1, x2) = [1] x2 + [7] 171.44/89.09 171.44/89.09 The order satisfies the following ordering constraints: 171.44/89.09 171.44/89.09 [lt(x, 0())] = [4] 171.44/89.09 > [1] 171.44/89.09 = [false()] 171.44/89.09 171.44/89.09 [lt(0(), s(x))] = [4] 171.44/89.09 > [1] 171.44/89.09 = [true()] 171.44/89.09 171.44/89.09 [lt(s(x), s(y))] = [4] 171.44/89.09 >= [4] 171.44/89.09 = [lt(x, y)] 171.44/89.09 171.44/89.09 [fac(x)] = [1] x + [7] 171.44/89.09 > [0] 171.44/89.09 = [help(x, 0())] 171.44/89.09 171.44/89.09 [help(x, c)] = [0] 171.44/89.09 ? [4] 171.44/89.09 = [if(lt(c, x), x, c)] 171.44/89.09 171.44/89.09 [if(true(), x, c)] = [1] 171.44/89.09 ? [7] 171.44/89.09 = [times(s(c), help(x, s(c)))] 171.44/89.09 171.44/89.09 [if(false(), x, c)] = [1] 171.44/89.09 > [0] 171.44/89.09 = [s(0())] 171.44/89.09 171.44/89.09 171.44/89.09 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 171.44/89.09 171.44/89.09 We are left with following problem, upon which TcT provides the 171.44/89.09 certificate MAYBE. 171.44/89.09 171.44/89.09 Strict Trs: 171.44/89.09 { lt(s(x), s(y)) -> lt(x, y) 171.44/89.09 , help(x, c) -> if(lt(c, x), x, c) 171.44/89.09 , if(true(), x, c) -> times(s(c), help(x, s(c))) } 171.44/89.09 Weak Trs: 171.44/89.09 { lt(x, 0()) -> false() 171.44/89.09 , lt(0(), s(x)) -> true() 171.44/89.09 , fac(x) -> help(x, 0()) 171.44/89.09 , if(false(), x, c) -> s(0()) } 171.44/89.09 Obligation: 171.44/89.09 runtime complexity 171.44/89.09 Answer: 171.44/89.09 MAYBE 171.44/89.09 171.44/89.09 The weightgap principle applies (using the following nonconstant 171.44/89.09 growth matrix-interpretation) 171.44/89.09 171.44/89.09 The following argument positions are usable: 171.44/89.09 Uargs(if) = {1}, Uargs(times) = {2} 171.44/89.09 171.44/89.09 TcT has computed the following matrix interpretation satisfying 171.44/89.09 not(EDA) and not(IDA(1)). 171.44/89.09 171.44/89.09 [lt](x1, x2) = [4] 171.44/89.09 171.44/89.09 [0] = [7] 171.44/89.09 171.44/89.09 [s](x1) = [0] 171.44/89.09 171.44/89.09 [true] = [0] 171.44/89.09 171.44/89.09 [false] = [0] 171.44/89.09 171.44/89.09 [fac](x1) = [1] x1 + [7] 171.44/89.09 171.44/89.09 [help](x1, x2) = [1] x1 + [5] 171.44/89.09 171.44/89.09 [if](x1, x2, x3) = [1] x1 + [1] x2 + [0] 171.44/89.09 171.44/89.09 [times](x1, x2) = [1] x2 + [6] 171.44/89.09 171.44/89.09 The order satisfies the following ordering constraints: 171.44/89.09 171.44/89.09 [lt(x, 0())] = [4] 171.44/89.09 > [0] 171.44/89.09 = [false()] 171.44/89.09 171.44/89.09 [lt(0(), s(x))] = [4] 171.44/89.09 > [0] 171.44/89.09 = [true()] 171.44/89.09 171.44/89.09 [lt(s(x), s(y))] = [4] 171.44/89.09 >= [4] 171.44/89.09 = [lt(x, y)] 171.44/89.09 171.44/89.09 [fac(x)] = [1] x + [7] 171.44/89.09 > [1] x + [5] 171.44/89.09 = [help(x, 0())] 171.44/89.09 171.44/89.09 [help(x, c)] = [1] x + [5] 171.44/89.09 > [1] x + [4] 171.44/89.09 = [if(lt(c, x), x, c)] 171.44/89.09 171.44/89.09 [if(true(), x, c)] = [1] x + [0] 171.44/89.09 ? [1] x + [11] 171.44/89.09 = [times(s(c), help(x, s(c)))] 171.44/89.09 171.44/89.09 [if(false(), x, c)] = [1] x + [0] 171.44/89.09 >= [0] 171.44/89.09 = [s(0())] 171.44/89.09 171.44/89.09 171.44/89.09 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 171.44/89.09 171.44/89.09 We are left with following problem, upon which TcT provides the 171.44/89.09 certificate MAYBE. 171.44/89.09 171.44/89.09 Strict Trs: 171.44/89.09 { lt(s(x), s(y)) -> lt(x, y) 171.44/89.09 , if(true(), x, c) -> times(s(c), help(x, s(c))) } 171.44/89.09 Weak Trs: 171.44/89.09 { lt(x, 0()) -> false() 171.44/89.09 , lt(0(), s(x)) -> true() 171.44/89.09 , fac(x) -> help(x, 0()) 171.44/89.09 , help(x, c) -> if(lt(c, x), x, c) 171.44/89.09 , if(false(), x, c) -> s(0()) } 171.44/89.09 Obligation: 171.44/89.09 runtime complexity 171.44/89.09 Answer: 171.44/89.09 MAYBE 171.44/89.09 171.44/89.09 None of the processors succeeded. 171.44/89.09 171.44/89.09 Details of failed attempt(s): 171.44/89.09 ----------------------------- 171.44/89.09 1) 'empty' failed due to the following reason: 171.44/89.09 171.44/89.09 Empty strict component of the problem is NOT empty. 171.44/89.09 171.44/89.09 2) 'With Problem ...' failed due to the following reason: 171.44/89.09 171.44/89.09 None of the processors succeeded. 171.44/89.09 171.44/89.09 Details of failed attempt(s): 171.44/89.09 ----------------------------- 171.44/89.09 1) 'empty' failed due to the following reason: 171.44/89.09 171.44/89.09 Empty strict component of the problem is NOT empty. 171.44/89.09 171.44/89.09 2) 'Fastest' failed due to the following reason: 171.44/89.09 171.44/89.09 None of the processors succeeded. 171.44/89.09 171.44/89.09 Details of failed attempt(s): 171.44/89.09 ----------------------------- 171.44/89.09 1) 'With Problem ...' failed due to the following reason: 171.44/89.09 171.44/89.09 None of the processors succeeded. 171.44/89.09 171.44/89.09 Details of failed attempt(s): 171.44/89.09 ----------------------------- 171.44/89.09 1) 'empty' failed due to the following reason: 171.44/89.09 171.44/89.09 Empty strict component of the problem is NOT empty. 171.44/89.09 171.44/89.09 2) 'With Problem ...' failed due to the following reason: 171.44/89.09 171.44/89.09 The weightgap principle applies (using the following nonconstant 171.44/89.09 growth matrix-interpretation) 171.44/89.09 171.44/89.09 The following argument positions are usable: 171.44/89.09 Uargs(if) = {1}, Uargs(times) = {2} 171.44/89.09 171.44/89.09 TcT has computed the following matrix interpretation satisfying 171.44/89.09 not(EDA) and not(IDA(1)). 171.44/89.09 171.44/89.09 [lt](x1, x2) = [0 0] x1 + [4] 171.44/89.09 [0 1] [0] 171.44/89.09 171.44/89.09 [0] = [0] 171.44/89.09 [1] 171.44/89.09 171.44/89.09 [s](x1) = [0] 171.44/89.09 [0] 171.44/89.09 171.44/89.09 [true] = [3] 171.44/89.09 [1] 171.44/89.09 171.44/89.09 [false] = [4] 171.44/89.09 [0] 171.44/89.09 171.44/89.09 [fac](x1) = [0 4] x1 + [7] 171.44/89.09 [0 0] [7] 171.44/89.09 171.44/89.09 [help](x1, x2) = [0 2] x2 + [4] 171.44/89.09 [0 0] [4] 171.44/89.09 171.44/89.09 [if](x1, x2, x3) = [1 2] x1 + [0] 171.44/89.09 [0 0] [0] 171.44/89.09 171.44/89.09 [times](x1, x2) = [1 0] x2 + [0] 171.44/89.09 [0 0] [0] 171.44/89.09 171.44/89.09 The order satisfies the following ordering constraints: 171.44/89.09 171.44/89.09 [lt(x, 0())] = [0 0] x + [4] 171.44/89.09 [0 1] [0] 171.44/89.09 >= [4] 171.44/89.09 [0] 171.44/89.09 = [false()] 171.44/89.09 171.44/89.09 [lt(0(), s(x))] = [4] 171.44/89.09 [1] 171.44/89.09 > [3] 171.44/89.09 [1] 171.44/89.09 = [true()] 171.44/89.09 171.44/89.09 [lt(s(x), s(y))] = [4] 171.44/89.09 [0] 171.44/89.09 ? [0 0] x + [4] 171.44/89.09 [0 1] [0] 171.44/89.09 = [lt(x, y)] 171.44/89.09 171.44/89.09 [fac(x)] = [0 4] x + [7] 171.44/89.09 [0 0] [7] 171.44/89.09 > [6] 171.44/89.09 [4] 171.44/89.09 = [help(x, 0())] 171.44/89.09 171.44/89.09 [help(x, c)] = [0 2] c + [4] 171.44/89.09 [0 0] [4] 171.44/89.09 >= [0 2] c + [4] 171.44/89.09 [0 0] [0] 171.44/89.09 = [if(lt(c, x), x, c)] 171.44/89.09 171.44/89.09 [if(true(), x, c)] = [5] 171.44/89.09 [0] 171.44/89.09 > [4] 171.44/89.09 [0] 171.44/89.09 = [times(s(c), help(x, s(c)))] 171.44/89.09 171.44/89.09 [if(false(), x, c)] = [4] 171.44/89.09 [0] 171.44/89.09 > [0] 171.44/89.09 [0] 171.44/89.09 = [s(0())] 171.44/89.09 171.44/89.09 171.44/89.09 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 171.44/89.09 171.44/89.09 We are left with following problem, upon which TcT provides the 171.44/89.09 certificate MAYBE. 171.44/89.09 171.44/89.09 Strict Trs: { lt(s(x), s(y)) -> lt(x, y) } 171.44/89.09 Weak Trs: 171.44/89.09 { lt(x, 0()) -> false() 171.44/89.09 , lt(0(), s(x)) -> true() 171.44/89.09 , fac(x) -> help(x, 0()) 171.44/89.09 , help(x, c) -> if(lt(c, x), x, c) 171.44/89.09 , if(true(), x, c) -> times(s(c), help(x, s(c))) 171.44/89.09 , if(false(), x, c) -> s(0()) } 171.44/89.09 Obligation: 171.44/89.09 runtime complexity 171.44/89.09 Answer: 171.44/89.09 MAYBE 171.44/89.09 171.44/89.09 None of the processors succeeded. 171.44/89.09 171.44/89.09 Details of failed attempt(s): 171.44/89.09 ----------------------------- 171.44/89.09 1) 'empty' failed due to the following reason: 171.44/89.09 171.44/89.09 Empty strict component of the problem is NOT empty. 171.44/89.09 171.44/89.09 2) 'With Problem ...' failed due to the following reason: 171.44/89.09 171.44/89.09 None of the processors succeeded. 171.44/89.09 171.44/89.09 Details of failed attempt(s): 171.44/89.09 ----------------------------- 171.44/89.09 1) 'empty' failed due to the following reason: 171.44/89.09 171.44/89.09 Empty strict component of the problem is NOT empty. 171.44/89.09 171.44/89.09 2) 'With Problem ...' failed due to the following reason: 171.44/89.09 171.44/89.09 Empty strict component of the problem is NOT empty. 171.44/89.09 171.44/89.09 171.44/89.09 171.44/89.09 171.44/89.09 2) 'With Problem ...' failed due to the following reason: 171.44/89.09 171.44/89.09 None of the processors succeeded. 171.44/89.09 171.44/89.09 Details of failed attempt(s): 171.44/89.09 ----------------------------- 171.44/89.09 1) 'empty' failed due to the following reason: 171.44/89.09 171.44/89.09 Empty strict component of the problem is NOT empty. 171.44/89.09 171.44/89.09 2) 'With Problem ...' failed due to the following reason: 171.44/89.09 171.44/89.09 Empty strict component of the problem is NOT empty. 171.44/89.09 171.44/89.09 171.44/89.09 171.44/89.09 171.44/89.09 171.44/89.09 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 171.44/89.09 failed due to the following reason: 171.44/89.09 171.44/89.09 None of the processors succeeded. 171.44/89.09 171.44/89.09 Details of failed attempt(s): 171.44/89.09 ----------------------------- 171.44/89.09 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 171.44/89.09 failed due to the following reason: 171.44/89.09 171.44/89.09 match-boundness of the problem could not be verified. 171.44/89.09 171.44/89.09 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 171.44/89.09 failed due to the following reason: 171.44/89.09 171.44/89.09 match-boundness of the problem could not be verified. 171.44/89.09 171.44/89.09 171.44/89.09 3) 'Best' failed due to the following reason: 171.44/89.09 171.44/89.09 None of the processors succeeded. 171.44/89.09 171.44/89.09 Details of failed attempt(s): 171.44/89.09 ----------------------------- 171.44/89.09 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 171.44/89.09 following reason: 171.44/89.09 171.44/89.09 The processor is inapplicable, reason: 171.44/89.09 Processor only applicable for innermost runtime complexity analysis 171.44/89.09 171.44/89.09 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 171.44/89.09 to the following reason: 171.44/89.09 171.44/89.09 The processor is inapplicable, reason: 171.44/89.09 Processor only applicable for innermost runtime complexity analysis 171.44/89.09 171.44/89.09 171.44/89.09 171.44/89.09 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 171.44/89.09 the following reason: 171.44/89.09 171.44/89.09 We add the following weak dependency pairs: 171.44/89.09 171.44/89.09 Strict DPs: 171.44/89.09 { lt^#(x, 0()) -> c_1() 171.44/89.09 , lt^#(0(), s(x)) -> c_2() 171.44/89.09 , lt^#(s(x), s(y)) -> c_3(lt^#(x, y)) 171.44/89.09 , fac^#(x) -> c_4(help^#(x, 0())) 171.44/89.09 , help^#(x, c) -> c_5(if^#(lt(c, x), x, c)) 171.44/89.09 , if^#(true(), x, c) -> c_6(c, help^#(x, s(c))) 171.44/89.09 , if^#(false(), x, c) -> c_7() } 171.44/89.09 171.44/89.09 and mark the set of starting terms. 171.44/89.09 171.44/89.09 We are left with following problem, upon which TcT provides the 171.44/89.09 certificate MAYBE. 171.44/89.09 171.44/89.09 Strict DPs: 171.44/89.09 { lt^#(x, 0()) -> c_1() 171.44/89.09 , lt^#(0(), s(x)) -> c_2() 171.44/89.09 , lt^#(s(x), s(y)) -> c_3(lt^#(x, y)) 171.44/89.09 , fac^#(x) -> c_4(help^#(x, 0())) 171.44/89.09 , help^#(x, c) -> c_5(if^#(lt(c, x), x, c)) 171.44/89.09 , if^#(true(), x, c) -> c_6(c, help^#(x, s(c))) 171.44/89.09 , if^#(false(), x, c) -> c_7() } 171.44/89.09 Strict Trs: 171.44/89.09 { lt(x, 0()) -> false() 171.44/89.09 , lt(0(), s(x)) -> true() 171.44/89.09 , lt(s(x), s(y)) -> lt(x, y) 171.44/89.09 , fac(x) -> help(x, 0()) 171.44/89.09 , help(x, c) -> if(lt(c, x), x, c) 171.44/89.09 , if(true(), x, c) -> times(s(c), help(x, s(c))) 171.44/89.09 , if(false(), x, c) -> s(0()) } 171.44/89.09 Obligation: 171.44/89.09 runtime complexity 171.44/89.09 Answer: 171.44/89.09 MAYBE 171.44/89.09 171.44/89.09 We estimate the number of application of {1,2,7} by applications of 171.44/89.09 Pre({1,2,7}) = {3,5,6}. Here rules are labeled as follows: 171.44/89.09 171.44/89.09 DPs: 171.44/89.09 { 1: lt^#(x, 0()) -> c_1() 171.44/89.09 , 2: lt^#(0(), s(x)) -> c_2() 171.44/89.09 , 3: lt^#(s(x), s(y)) -> c_3(lt^#(x, y)) 171.44/89.09 , 4: fac^#(x) -> c_4(help^#(x, 0())) 171.44/89.09 , 5: help^#(x, c) -> c_5(if^#(lt(c, x), x, c)) 171.44/89.09 , 6: if^#(true(), x, c) -> c_6(c, help^#(x, s(c))) 171.44/89.09 , 7: if^#(false(), x, c) -> c_7() } 171.44/89.09 171.44/89.09 We are left with following problem, upon which TcT provides the 171.44/89.09 certificate MAYBE. 171.44/89.09 171.44/89.09 Strict DPs: 171.44/89.09 { lt^#(s(x), s(y)) -> c_3(lt^#(x, y)) 171.44/89.09 , fac^#(x) -> c_4(help^#(x, 0())) 171.44/89.09 , help^#(x, c) -> c_5(if^#(lt(c, x), x, c)) 171.44/89.09 , if^#(true(), x, c) -> c_6(c, help^#(x, s(c))) } 171.44/89.09 Strict Trs: 171.44/89.09 { lt(x, 0()) -> false() 171.44/89.09 , lt(0(), s(x)) -> true() 171.44/89.09 , lt(s(x), s(y)) -> lt(x, y) 171.44/89.09 , fac(x) -> help(x, 0()) 171.44/89.09 , help(x, c) -> if(lt(c, x), x, c) 171.44/89.09 , if(true(), x, c) -> times(s(c), help(x, s(c))) 171.44/89.09 , if(false(), x, c) -> s(0()) } 171.44/89.09 Weak DPs: 171.44/89.09 { lt^#(x, 0()) -> c_1() 171.44/89.09 , lt^#(0(), s(x)) -> c_2() 171.44/89.09 , if^#(false(), x, c) -> c_7() } 171.44/89.09 Obligation: 171.44/89.09 runtime complexity 171.44/89.09 Answer: 171.44/89.09 MAYBE 171.44/89.09 171.44/89.09 Empty strict component of the problem is NOT empty. 171.44/89.09 171.44/89.09 171.44/89.09 Arrrr.. 171.79/89.30 EOF