MAYBE 122.87/50.06 MAYBE 122.87/50.06 122.87/50.06 We are left with following problem, upon which TcT provides the 122.87/50.06 certificate MAYBE. 122.87/50.06 122.87/50.06 Strict Trs: 122.87/50.06 { fac(s(x)) -> *(fac(p(s(x))), s(x)) 122.87/50.06 , p(s(s(x))) -> s(p(s(x))) 122.87/50.06 , p(s(0())) -> 0() } 122.87/50.06 Obligation: 122.87/50.06 runtime complexity 122.87/50.06 Answer: 122.87/50.06 MAYBE 122.87/50.06 122.87/50.06 None of the processors succeeded. 122.87/50.06 122.87/50.06 Details of failed attempt(s): 122.87/50.06 ----------------------------- 122.87/50.06 1) 'Best' failed due to the following reason: 122.87/50.06 122.87/50.06 None of the processors succeeded. 122.87/50.06 122.87/50.06 Details of failed attempt(s): 122.87/50.06 ----------------------------- 122.87/50.06 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 122.87/50.06 seconds)' failed due to the following reason: 122.87/50.06 122.87/50.06 None of the processors succeeded. 122.87/50.06 122.87/50.06 Details of failed attempt(s): 122.87/50.06 ----------------------------- 122.87/50.06 1) 'empty' failed due to the following reason: 122.87/50.06 122.87/50.06 Empty strict component of the problem is NOT empty. 122.87/50.06 122.87/50.06 2) 'With Problem ...' failed due to the following reason: 122.87/50.06 122.87/50.06 None of the processors succeeded. 122.87/50.06 122.87/50.06 Details of failed attempt(s): 122.87/50.06 ----------------------------- 122.87/50.06 1) 'empty' failed due to the following reason: 122.87/50.06 122.87/50.06 Empty strict component of the problem is NOT empty. 122.87/50.06 122.87/50.06 2) 'Fastest' failed due to the following reason: 122.87/50.06 122.87/50.06 None of the processors succeeded. 122.87/50.06 122.87/50.06 Details of failed attempt(s): 122.87/50.06 ----------------------------- 122.87/50.06 1) 'With Problem ...' failed due to the following reason: 122.87/50.06 122.87/50.06 None of the processors succeeded. 122.87/50.06 122.87/50.06 Details of failed attempt(s): 122.87/50.06 ----------------------------- 122.87/50.06 1) 'empty' failed due to the following reason: 122.87/50.06 122.87/50.06 Empty strict component of the problem is NOT empty. 122.87/50.06 122.87/50.06 2) 'With Problem ...' failed due to the following reason: 122.87/50.06 122.87/50.06 None of the processors succeeded. 122.87/50.06 122.87/50.06 Details of failed attempt(s): 122.87/50.06 ----------------------------- 122.87/50.06 1) 'empty' failed due to the following reason: 122.87/50.06 122.87/50.06 Empty strict component of the problem is NOT empty. 122.87/50.06 122.87/50.06 2) 'With Problem ...' failed due to the following reason: 122.87/50.06 122.87/50.06 We use the processor 'matrix interpretation of dimension 3' to 122.87/50.06 orient following rules strictly. 122.87/50.06 122.87/50.06 Trs: { fac(s(x)) -> *(fac(p(s(x))), s(x)) } 122.87/50.06 122.87/50.06 The induced complexity on above rules (modulo remaining rules) is 122.87/50.06 YES(?,O(n^3)) . These rules are moved into the corresponding weak 122.87/50.06 component(s). 122.87/50.06 122.87/50.06 Sub-proof: 122.87/50.06 ---------- 122.87/50.06 TcT has computed the following constructor-based matrix 122.87/50.06 interpretation satisfying not(EDA). 122.87/50.06 122.87/50.06 [4 2 5] [0] 122.87/50.06 [fac](x1) = [0 0 4] x1 + [0] 122.87/50.06 [0 0 0] [0] 122.87/50.06 122.87/50.06 [1 0 0] [0] 122.87/50.06 [s](x1) = [0 0 1] x1 + [0] 122.87/50.06 [1 0 1] [2] 122.87/50.06 122.87/50.06 [1 0 0] [1 0 0] [5] 122.87/50.06 [*](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [3] 122.87/50.06 [0 0 0] [0 0 0] [0] 122.87/50.06 122.87/50.06 [1 0 0] [0] 122.87/50.06 [p](x1) = [2 1 0] x1 + [0] 122.87/50.06 [0 1 0] [0] 122.87/50.06 122.87/50.06 [0] 122.87/50.06 [0] = [0] 122.87/50.06 [0] 122.87/50.06 122.87/50.06 The order satisfies the following ordering constraints: 122.87/50.06 122.87/50.06 [fac(s(x))] = [9 0 7] [10] 122.87/50.06 [4 0 4] x + [8] 122.87/50.06 [0 0 0] [0] 122.87/50.06 > [9 0 7] [5] 122.87/50.06 [0 0 0] x + [3] 122.87/50.06 [0 0 0] [0] 122.87/50.06 = [*(fac(p(s(x))), s(x))] 122.87/50.06 122.87/50.06 [p(s(s(x)))] = [1 0 0] [0] 122.87/50.06 [3 0 1] x + [2] 122.87/50.06 [1 0 1] [2] 122.87/50.06 >= [1 0 0] [0] 122.87/50.06 [0 0 1] x + [0] 122.87/50.06 [1 0 1] [2] 122.87/50.06 = [s(p(s(x)))] 122.87/50.06 122.87/50.06 [p(s(0()))] = [0] 122.87/50.06 [0] 122.87/50.06 [0] 122.87/50.06 >= [0] 122.87/50.06 [0] 122.87/50.06 [0] 122.87/50.06 = [0()] 122.87/50.06 122.87/50.06 122.87/50.06 We return to the main proof. 122.87/50.06 122.87/50.06 We are left with following problem, upon which TcT provides the 122.87/50.06 certificate MAYBE. 122.87/50.06 122.87/50.06 Strict Trs: 122.87/50.06 { p(s(s(x))) -> s(p(s(x))) 122.87/50.06 , p(s(0())) -> 0() } 122.87/50.06 Weak Trs: { fac(s(x)) -> *(fac(p(s(x))), s(x)) } 122.87/50.06 Obligation: 122.87/50.06 runtime complexity 122.87/50.06 Answer: 122.87/50.06 MAYBE 122.87/50.06 122.87/50.06 None of the processors succeeded. 122.87/50.06 122.87/50.06 Details of failed attempt(s): 122.87/50.06 ----------------------------- 122.87/50.06 1) 'empty' failed due to the following reason: 122.87/50.06 122.87/50.06 Empty strict component of the problem is NOT empty. 122.87/50.06 122.87/50.06 2) 'With Problem ...' failed due to the following reason: 122.87/50.06 122.87/50.06 Empty strict component of the problem is NOT empty. 122.87/50.06 122.87/50.06 122.87/50.06 122.87/50.06 122.87/50.06 2) 'With Problem ...' failed due to the following reason: 122.87/50.06 122.87/50.06 None of the processors succeeded. 122.87/50.06 122.87/50.06 Details of failed attempt(s): 122.87/50.06 ----------------------------- 122.87/50.06 1) 'empty' failed due to the following reason: 122.87/50.06 122.87/50.06 Empty strict component of the problem is NOT empty. 122.87/50.06 122.87/50.06 2) 'With Problem ...' failed due to the following reason: 122.87/50.06 122.87/50.06 Empty strict component of the problem is NOT empty. 122.87/50.06 122.87/50.06 122.87/50.06 122.87/50.06 122.87/50.06 122.87/50.06 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 122.87/50.06 failed due to the following reason: 122.87/50.06 122.87/50.06 None of the processors succeeded. 122.87/50.06 122.87/50.06 Details of failed attempt(s): 122.87/50.06 ----------------------------- 122.87/50.06 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 122.87/50.06 failed due to the following reason: 122.87/50.06 122.87/50.06 match-boundness of the problem could not be verified. 122.87/50.06 122.87/50.06 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 122.87/50.06 failed due to the following reason: 122.87/50.06 122.87/50.06 match-boundness of the problem could not be verified. 122.87/50.06 122.87/50.06 122.87/50.06 3) 'Best' failed due to the following reason: 122.87/50.06 122.87/50.06 None of the processors succeeded. 122.87/50.06 122.87/50.06 Details of failed attempt(s): 122.87/50.06 ----------------------------- 122.87/50.06 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 122.87/50.06 following reason: 122.87/50.06 122.87/50.06 The processor is inapplicable, reason: 122.87/50.06 Processor only applicable for innermost runtime complexity analysis 122.87/50.06 122.87/50.06 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 122.87/50.06 to the following reason: 122.87/50.06 122.87/50.06 The processor is inapplicable, reason: 122.87/50.06 Processor only applicable for innermost runtime complexity analysis 122.87/50.06 122.87/50.06 122.87/50.06 122.87/50.06 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 122.87/50.06 the following reason: 122.87/50.06 122.87/50.06 We add the following weak dependency pairs: 122.87/50.06 122.87/50.06 Strict DPs: 122.87/50.06 { fac^#(s(x)) -> c_1(fac^#(p(s(x))), x) 122.87/50.06 , p^#(s(s(x))) -> c_2(p^#(s(x))) 122.87/50.06 , p^#(s(0())) -> c_3() } 122.87/50.06 122.87/50.06 and mark the set of starting terms. 122.87/50.06 122.87/50.06 We are left with following problem, upon which TcT provides the 122.87/50.06 certificate MAYBE. 122.87/50.06 122.87/50.06 Strict DPs: 122.87/50.06 { fac^#(s(x)) -> c_1(fac^#(p(s(x))), x) 122.87/50.06 , p^#(s(s(x))) -> c_2(p^#(s(x))) 122.87/50.06 , p^#(s(0())) -> c_3() } 122.87/50.06 Strict Trs: 122.87/50.06 { fac(s(x)) -> *(fac(p(s(x))), s(x)) 122.87/50.06 , p(s(s(x))) -> s(p(s(x))) 122.87/50.06 , p(s(0())) -> 0() } 122.87/50.06 Obligation: 122.87/50.06 runtime complexity 122.87/50.06 Answer: 122.87/50.06 MAYBE 122.87/50.06 122.87/50.06 We estimate the number of application of {3} by applications of 122.87/50.06 Pre({3}) = {1,2}. Here rules are labeled as follows: 122.87/50.06 122.87/50.06 DPs: 122.87/50.06 { 1: fac^#(s(x)) -> c_1(fac^#(p(s(x))), x) 122.87/50.06 , 2: p^#(s(s(x))) -> c_2(p^#(s(x))) 122.87/50.06 , 3: p^#(s(0())) -> c_3() } 122.87/50.06 122.87/50.06 We are left with following problem, upon which TcT provides the 122.87/50.06 certificate MAYBE. 122.87/50.06 122.87/50.06 Strict DPs: 122.87/50.06 { fac^#(s(x)) -> c_1(fac^#(p(s(x))), x) 122.87/50.06 , p^#(s(s(x))) -> c_2(p^#(s(x))) } 122.87/50.06 Strict Trs: 122.87/50.06 { fac(s(x)) -> *(fac(p(s(x))), s(x)) 122.87/50.06 , p(s(s(x))) -> s(p(s(x))) 122.87/50.06 , p(s(0())) -> 0() } 122.87/50.06 Weak DPs: { p^#(s(0())) -> c_3() } 122.87/50.06 Obligation: 122.87/50.06 runtime complexity 122.87/50.06 Answer: 122.87/50.06 MAYBE 122.87/50.06 122.87/50.06 Empty strict component of the problem is NOT empty. 122.87/50.06 122.87/50.06 122.87/50.06 Arrrr.. 123.11/50.20 EOF