MAYBE 550.32/148.03 MAYBE 550.32/148.03 550.32/148.03 We are left with following problem, upon which TcT provides the 550.32/148.03 certificate MAYBE. 550.32/148.03 550.32/148.03 Strict Trs: 550.32/148.03 { equal0(Nil()) -> number42(Nil()) 550.32/148.03 , equal0(Cons(x, xs)) -> equal0(Cons(x, xs)) 550.32/148.03 , number42(x) -> 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Nil())))))))))))))))))))))))))))))))))))))))))) 550.32/148.03 , goal(x) -> equal0(x) } 550.32/148.03 Obligation: 550.32/148.03 innermost runtime complexity 550.32/148.03 Answer: 550.32/148.03 MAYBE 550.32/148.03 550.32/148.03 None of the processors succeeded. 550.32/148.03 550.32/148.03 Details of failed attempt(s): 550.32/148.03 ----------------------------- 550.32/148.03 1) 'empty' failed due to the following reason: 550.32/148.03 550.32/148.03 Empty strict component of the problem is NOT empty. 550.32/148.03 550.32/148.03 2) 'Best' failed due to the following reason: 550.32/148.03 550.32/148.03 None of the processors succeeded. 550.32/148.03 550.32/148.03 Details of failed attempt(s): 550.32/148.03 ----------------------------- 550.32/148.03 1) 'Best' failed due to the following reason: 550.32/148.03 550.32/148.03 None of the processors succeeded. 550.32/148.03 550.32/148.03 Details of failed attempt(s): 550.32/148.03 ----------------------------- 550.32/148.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 550.32/148.03 seconds)' failed due to the following reason: 550.32/148.03 550.32/148.03 Computation stopped due to timeout after 148.0 seconds. 550.32/148.03 550.32/148.03 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 550.32/148.03 failed due to the following reason: 550.32/148.03 550.32/148.03 Computation stopped due to timeout after 24.0 seconds. 550.32/148.03 550.32/148.03 3) 'Best' failed due to the following reason: 550.32/148.03 550.32/148.03 None of the processors succeeded. 550.32/148.03 550.32/148.03 Details of failed attempt(s): 550.32/148.03 ----------------------------- 550.32/148.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 550.32/148.03 following reason: 550.32/148.03 550.32/148.03 The input cannot be shown compatible 550.32/148.03 550.32/148.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 550.32/148.03 to the following reason: 550.32/148.03 550.32/148.03 The input cannot be shown compatible 550.32/148.03 550.32/148.03 550.32/148.03 550.32/148.03 2) 'With Problem ... (timeout of 297 seconds)' failed due to the 550.32/148.03 following reason: 550.32/148.03 550.32/148.03 We add the following weak dependency pairs: 550.32/148.03 550.32/148.03 Strict DPs: 550.32/148.03 { equal0^#(Nil()) -> c_1(number42^#(Nil())) 550.32/148.03 , equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) 550.32/148.03 , number42^#(x) -> c_3() 550.32/148.03 , goal^#(x) -> c_4(equal0^#(x)) } 550.32/148.03 550.32/148.03 and mark the set of starting terms. 550.32/148.03 550.32/148.03 We are left with following problem, upon which TcT provides the 550.32/148.03 certificate MAYBE. 550.32/148.03 550.32/148.03 Strict DPs: 550.32/148.03 { equal0^#(Nil()) -> c_1(number42^#(Nil())) 550.32/148.03 , equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) 550.32/148.03 , number42^#(x) -> c_3() 550.32/148.03 , goal^#(x) -> c_4(equal0^#(x)) } 550.32/148.03 Strict Trs: 550.32/148.03 { equal0(Nil()) -> number42(Nil()) 550.32/148.03 , equal0(Cons(x, xs)) -> equal0(Cons(x, xs)) 550.32/148.03 , number42(x) -> 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.03 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Cons(Nil(), 550.32/148.04 Nil())))))))))))))))))))))))))))))))))))))))))) 550.32/148.04 , goal(x) -> equal0(x) } 550.32/148.04 Obligation: 550.32/148.04 innermost runtime complexity 550.32/148.04 Answer: 550.32/148.04 MAYBE 550.32/148.04 550.32/148.04 No rule is usable, rules are removed from the input problem. 550.32/148.04 550.32/148.04 We are left with following problem, upon which TcT provides the 550.32/148.04 certificate MAYBE. 550.32/148.04 550.32/148.04 Strict DPs: 550.32/148.04 { equal0^#(Nil()) -> c_1(number42^#(Nil())) 550.32/148.04 , equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) 550.32/148.04 , number42^#(x) -> c_3() 550.32/148.04 , goal^#(x) -> c_4(equal0^#(x)) } 550.32/148.04 Obligation: 550.32/148.04 innermost runtime complexity 550.32/148.04 Answer: 550.32/148.04 MAYBE 550.32/148.04 550.32/148.04 The weightgap principle applies (using the following constant 550.32/148.04 growth matrix-interpretation) 550.32/148.04 550.32/148.04 The following argument positions are usable: 550.32/148.04 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_4) = {1} 550.32/148.04 550.32/148.04 TcT has computed the following constructor-restricted matrix 550.32/148.04 interpretation. 550.32/148.04 550.32/148.04 [Nil] = [0] 550.32/148.04 [0] 550.32/148.04 550.32/148.04 [Cons](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 550.32/148.04 [0 0] [0 0] [0] 550.32/148.04 550.32/148.04 [equal0^#](x1) = [0] 550.32/148.04 [0] 550.32/148.04 550.32/148.04 [c_1](x1) = [1 0] x1 + [1] 550.32/148.04 [0 1] [0] 550.32/148.04 550.32/148.04 [number42^#](x1) = [1 2] x1 + [0] 550.32/148.04 [2 1] [0] 550.32/148.04 550.32/148.04 [c_2](x1) = [1 0] x1 + [1] 550.32/148.04 [0 1] [1] 550.32/148.04 550.32/148.04 [c_3] = [1] 550.32/148.04 [0] 550.32/148.04 550.32/148.04 [goal^#](x1) = [1 2] x1 + [2] 550.32/148.04 [2 1] [2] 550.32/148.04 550.32/148.04 [c_4](x1) = [1 0] x1 + [1] 550.32/148.04 [0 1] [2] 550.32/148.04 550.32/148.04 The order satisfies the following ordering constraints: 550.32/148.04 550.32/148.04 [equal0^#(Nil())] = [0] 550.32/148.04 [0] 550.32/148.04 ? [1] 550.32/148.04 [0] 550.32/148.04 = [c_1(number42^#(Nil()))] 550.32/148.04 550.32/148.04 [equal0^#(Cons(x, xs))] = [0] 550.32/148.04 [0] 550.32/148.04 ? [1] 550.32/148.04 [1] 550.32/148.04 = [c_2(equal0^#(Cons(x, xs)))] 550.32/148.04 550.32/148.04 [number42^#(x)] = [1 2] x + [0] 550.32/148.04 [2 1] [0] 550.32/148.04 ? [1] 550.32/148.04 [0] 550.32/148.04 = [c_3()] 550.32/148.04 550.32/148.04 [goal^#(x)] = [1 2] x + [2] 550.32/148.04 [2 1] [2] 550.32/148.04 > [1] 550.32/148.04 [2] 550.32/148.04 = [c_4(equal0^#(x))] 550.32/148.04 550.32/148.04 550.32/148.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 550.32/148.04 550.32/148.04 We are left with following problem, upon which TcT provides the 550.32/148.04 certificate MAYBE. 550.32/148.04 550.32/148.04 Strict DPs: 550.32/148.04 { equal0^#(Nil()) -> c_1(number42^#(Nil())) 550.32/148.04 , equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) 550.32/148.04 , number42^#(x) -> c_3() } 550.32/148.04 Weak DPs: { goal^#(x) -> c_4(equal0^#(x)) } 550.32/148.04 Obligation: 550.32/148.04 innermost runtime complexity 550.32/148.04 Answer: 550.32/148.04 MAYBE 550.32/148.04 550.32/148.04 We estimate the number of application of {3} by applications of 550.32/148.04 Pre({3}) = {1}. Here rules are labeled as follows: 550.32/148.04 550.32/148.04 DPs: 550.32/148.04 { 1: equal0^#(Nil()) -> c_1(number42^#(Nil())) 550.32/148.04 , 2: equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) 550.32/148.04 , 3: number42^#(x) -> c_3() 550.32/148.04 , 4: goal^#(x) -> c_4(equal0^#(x)) } 550.32/148.04 550.32/148.04 We are left with following problem, upon which TcT provides the 550.32/148.04 certificate MAYBE. 550.32/148.04 550.32/148.04 Strict DPs: 550.32/148.04 { equal0^#(Nil()) -> c_1(number42^#(Nil())) 550.32/148.04 , equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) } 550.32/148.04 Weak DPs: 550.32/148.04 { number42^#(x) -> c_3() 550.32/148.04 , goal^#(x) -> c_4(equal0^#(x)) } 550.32/148.04 Obligation: 550.32/148.04 innermost runtime complexity 550.32/148.04 Answer: 550.32/148.04 MAYBE 550.32/148.04 550.32/148.04 The following weak DPs constitute a sub-graph of the DG that is 550.32/148.04 closed under successors. The DPs are removed. 550.32/148.04 550.32/148.04 { number42^#(x) -> c_3() } 550.32/148.04 550.32/148.04 We are left with following problem, upon which TcT provides the 550.32/148.04 certificate MAYBE. 550.32/148.04 550.32/148.04 Strict DPs: 550.32/148.04 { equal0^#(Nil()) -> c_1(number42^#(Nil())) 550.32/148.04 , equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) } 550.32/148.04 Weak DPs: { goal^#(x) -> c_4(equal0^#(x)) } 550.32/148.04 Obligation: 550.32/148.04 innermost runtime complexity 550.32/148.04 Answer: 550.32/148.04 MAYBE 550.32/148.04 550.32/148.04 Due to missing edges in the dependency-graph, the right-hand sides 550.32/148.04 of following rules could be simplified: 550.32/148.04 550.32/148.04 { equal0^#(Nil()) -> c_1(number42^#(Nil())) } 550.32/148.04 550.32/148.04 We are left with following problem, upon which TcT provides the 550.32/148.04 certificate MAYBE. 550.32/148.04 550.32/148.04 Strict DPs: 550.32/148.04 { equal0^#(Nil()) -> c_1() 550.32/148.04 , equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) } 550.32/148.04 Weak DPs: { goal^#(x) -> c_3(equal0^#(x)) } 550.32/148.04 Obligation: 550.32/148.04 innermost runtime complexity 550.32/148.04 Answer: 550.32/148.04 MAYBE 550.32/148.04 550.32/148.04 Consider the dependency graph 550.32/148.04 550.32/148.04 1: equal0^#(Nil()) -> c_1() 550.32/148.04 550.32/148.04 2: equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) 550.32/148.04 -->_1 equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) :2 550.32/148.04 550.32/148.04 3: goal^#(x) -> c_3(equal0^#(x)) 550.32/148.04 -->_1 equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) :2 550.32/148.04 -->_1 equal0^#(Nil()) -> c_1() :1 550.32/148.04 550.32/148.04 550.32/148.04 Following roots of the dependency graph are removed, as the 550.32/148.04 considered set of starting terms is closed under reduction with 550.32/148.04 respect to these rules (modulo compound contexts). 550.32/148.04 550.32/148.04 { goal^#(x) -> c_3(equal0^#(x)) } 550.32/148.04 550.32/148.04 550.32/148.04 We are left with following problem, upon which TcT provides the 550.32/148.04 certificate MAYBE. 550.32/148.04 550.32/148.04 Strict DPs: 550.32/148.04 { equal0^#(Nil()) -> c_1() 550.32/148.04 , equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) } 550.32/148.04 Obligation: 550.32/148.04 innermost runtime complexity 550.32/148.04 Answer: 550.32/148.04 MAYBE 550.32/148.04 550.32/148.04 Consider the dependency graph 550.32/148.04 550.32/148.04 1: equal0^#(Nil()) -> c_1() 550.32/148.04 550.32/148.04 2: equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) 550.32/148.04 -->_1 equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) :2 550.32/148.04 550.32/148.04 550.32/148.04 Following roots of the dependency graph are removed, as the 550.32/148.04 considered set of starting terms is closed under reduction with 550.32/148.04 respect to these rules (modulo compound contexts). 550.32/148.04 550.32/148.04 { equal0^#(Nil()) -> c_1() } 550.32/148.04 550.32/148.04 550.32/148.04 We are left with following problem, upon which TcT provides the 550.32/148.04 certificate MAYBE. 550.32/148.04 550.32/148.04 Strict DPs: { equal0^#(Cons(x, xs)) -> c_2(equal0^#(Cons(x, xs))) } 550.32/148.04 Obligation: 550.32/148.04 innermost runtime complexity 550.32/148.04 Answer: 550.32/148.04 MAYBE 550.32/148.04 550.32/148.04 None of the processors succeeded. 550.32/148.04 550.32/148.04 Details of failed attempt(s): 550.32/148.04 ----------------------------- 550.32/148.04 1) 'empty' failed due to the following reason: 550.32/148.04 550.32/148.04 Empty strict component of the problem is NOT empty. 550.32/148.04 550.32/148.04 2) 'With Problem ...' failed due to the following reason: 550.32/148.04 550.32/148.04 None of the processors succeeded. 550.32/148.04 550.32/148.04 Details of failed attempt(s): 550.32/148.04 ----------------------------- 550.32/148.04 1) 'empty' failed due to the following reason: 550.32/148.04 550.32/148.04 Empty strict component of the problem is NOT empty. 550.32/148.04 550.32/148.04 2) 'Fastest' failed due to the following reason: 550.32/148.04 550.32/148.04 None of the processors succeeded. 550.32/148.04 550.32/148.04 Details of failed attempt(s): 550.32/148.04 ----------------------------- 550.32/148.04 1) 'With Problem ...' failed due to the following reason: 550.32/148.04 550.32/148.04 None of the processors succeeded. 550.32/148.04 550.32/148.04 Details of failed attempt(s): 550.32/148.04 ----------------------------- 550.32/148.04 1) 'empty' failed due to the following reason: 550.32/148.04 550.32/148.04 Empty strict component of the problem is NOT empty. 550.32/148.04 550.32/148.04 2) 'Polynomial Path Order (PS)' failed due to the following reason: 550.32/148.04 550.32/148.04 The input cannot be shown compatible 550.32/148.04 550.32/148.04 550.32/148.04 2) 'Fastest (timeout of 24 seconds)' failed due to the following 550.32/148.04 reason: 550.32/148.04 550.32/148.04 Computation stopped due to timeout after 24.0 seconds. 550.32/148.04 550.32/148.04 3) 'Polynomial Path Order (PS)' failed due to the following reason: 550.32/148.04 550.32/148.04 The input cannot be shown compatible 550.32/148.04 550.32/148.04 550.32/148.04 550.32/148.04 550.32/148.04 550.32/148.04 550.32/148.04 Arrrr.. 550.51/148.16 EOF