MAYBE 1148.69/298.78 MAYBE 1148.69/298.78 1148.69/298.78 We are left with following problem, upon which TcT provides the 1148.69/298.78 certificate MAYBE. 1148.69/298.78 1148.69/298.78 Strict Trs: 1148.69/298.78 { a__first(X1, X2) -> first(X1, X2) 1148.69/298.78 , a__first(0(), X) -> nil() 1148.69/298.78 , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)) 1148.69/298.78 , mark(0()) -> 0() 1148.69/298.78 , mark(nil()) -> nil() 1148.69/298.78 , mark(s(X)) -> s(mark(X)) 1148.69/298.78 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 1148.69/298.78 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1148.69/298.78 , mark(from(X)) -> a__from(mark(X)) 1148.69/298.78 , a__from(X) -> cons(mark(X), from(s(X))) 1148.69/298.78 , a__from(X) -> from(X) } 1148.69/298.78 Obligation: 1148.69/298.78 runtime complexity 1148.69/298.78 Answer: 1148.69/298.78 MAYBE 1148.69/298.78 1148.69/298.78 None of the processors succeeded. 1148.69/298.78 1148.69/298.78 Details of failed attempt(s): 1148.69/298.78 ----------------------------- 1148.69/298.78 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1148.69/298.78 following reason: 1148.69/298.78 1148.69/298.78 Computation stopped due to timeout after 297.0 seconds. 1148.69/298.78 1148.69/298.78 2) 'Best' failed due to the following reason: 1148.69/298.78 1148.69/298.78 None of the processors succeeded. 1148.69/298.78 1148.69/298.78 Details of failed attempt(s): 1148.69/298.78 ----------------------------- 1148.69/298.78 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1148.69/298.79 seconds)' failed due to the following reason: 1148.69/298.79 1148.69/298.79 None of the processors succeeded. 1148.69/298.79 1148.69/298.79 Details of failed attempt(s): 1148.69/298.79 ----------------------------- 1148.69/298.79 1) 'empty' failed due to the following reason: 1148.69/298.79 1148.69/298.79 Empty strict component of the problem is NOT empty. 1148.69/298.79 1148.69/298.79 2) 'With Problem ...' failed due to the following reason: 1148.69/298.79 1148.69/298.79 None of the processors succeeded. 1148.69/298.79 1148.69/298.79 Details of failed attempt(s): 1148.69/298.79 ----------------------------- 1148.69/298.79 1) 'empty' failed due to the following reason: 1148.69/298.79 1148.69/298.79 Empty strict component of the problem is NOT empty. 1148.69/298.79 1148.69/298.79 2) 'Fastest' failed due to the following reason: 1148.69/298.79 1148.69/298.79 None of the processors succeeded. 1148.69/298.79 1148.69/298.79 Details of failed attempt(s): 1148.69/298.79 ----------------------------- 1148.69/298.79 1) 'With Problem ...' failed due to the following reason: 1148.69/298.79 1148.69/298.79 None of the processors succeeded. 1148.69/298.79 1148.69/298.79 Details of failed attempt(s): 1148.69/298.79 ----------------------------- 1148.69/298.79 1) 'empty' failed due to the following reason: 1148.69/298.79 1148.69/298.79 Empty strict component of the problem is NOT empty. 1148.69/298.79 1148.69/298.79 2) 'With Problem ...' failed due to the following reason: 1148.69/298.79 1148.69/298.79 None of the processors succeeded. 1148.69/298.79 1148.69/298.79 Details of failed attempt(s): 1148.69/298.79 ----------------------------- 1148.69/298.79 1) 'empty' failed due to the following reason: 1148.69/298.79 1148.69/298.79 Empty strict component of the problem is NOT empty. 1148.69/298.79 1148.69/298.79 2) 'With Problem ...' failed due to the following reason: 1148.69/298.79 1148.69/298.79 None of the processors succeeded. 1148.69/298.79 1148.69/298.79 Details of failed attempt(s): 1148.69/298.79 ----------------------------- 1148.69/298.79 1) 'empty' failed due to the following reason: 1148.69/298.79 1148.69/298.79 Empty strict component of the problem is NOT empty. 1148.69/298.79 1148.69/298.79 2) 'With Problem ...' failed due to the following reason: 1148.69/298.79 1148.69/298.79 Empty strict component of the problem is NOT empty. 1148.69/298.79 1148.69/298.79 1148.69/298.79 1148.69/298.79 1148.69/298.79 2) 'With Problem ...' failed due to the following reason: 1148.69/298.79 1148.69/298.79 None of the processors succeeded. 1148.69/298.79 1148.69/298.79 Details of failed attempt(s): 1148.69/298.79 ----------------------------- 1148.69/298.79 1) 'empty' failed due to the following reason: 1148.69/298.79 1148.69/298.79 Empty strict component of the problem is NOT empty. 1148.69/298.79 1148.69/298.79 2) 'With Problem ...' failed due to the following reason: 1148.69/298.79 1148.69/298.79 Empty strict component of the problem is NOT empty. 1148.69/298.79 1148.69/298.79 1148.69/298.79 1148.69/298.79 1148.69/298.79 1148.69/298.79 2) 'Best' failed due to the following reason: 1148.69/298.79 1148.69/298.79 None of the processors succeeded. 1148.69/298.79 1148.69/298.79 Details of failed attempt(s): 1148.69/298.79 ----------------------------- 1148.69/298.79 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1148.69/298.79 to the following reason: 1148.69/298.79 1148.69/298.79 The processor is inapplicable, reason: 1148.69/298.79 Processor only applicable for innermost runtime complexity analysis 1148.69/298.79 1148.69/298.79 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1148.69/298.79 following reason: 1148.69/298.79 1148.69/298.79 The processor is inapplicable, reason: 1148.69/298.79 Processor only applicable for innermost runtime complexity analysis 1148.69/298.79 1148.69/298.79 1148.69/298.79 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1148.69/298.79 failed due to the following reason: 1148.69/298.79 1148.69/298.79 None of the processors succeeded. 1148.69/298.79 1148.69/298.79 Details of failed attempt(s): 1148.69/298.79 ----------------------------- 1148.69/298.79 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1148.69/298.79 failed due to the following reason: 1148.69/298.79 1148.69/298.79 match-boundness of the problem could not be verified. 1148.69/298.79 1148.69/298.79 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1148.69/298.79 failed due to the following reason: 1148.69/298.79 1148.69/298.79 match-boundness of the problem could not be verified. 1148.69/298.79 1148.69/298.79 1148.69/298.79 1148.69/298.79 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1148.69/298.79 the following reason: 1148.69/298.79 1148.69/298.79 We add the following weak dependency pairs: 1148.69/298.79 1148.69/298.79 Strict DPs: 1148.69/298.79 { a__first^#(X1, X2) -> c_1(X1, X2) 1148.69/298.79 , a__first^#(0(), X) -> c_2() 1148.69/298.79 , a__first^#(s(X), cons(Y, Z)) -> c_3(mark^#(Y), X, Z) 1148.69/298.79 , mark^#(0()) -> c_4() 1148.69/298.79 , mark^#(nil()) -> c_5() 1148.69/298.79 , mark^#(s(X)) -> c_6(mark^#(X)) 1148.69/298.79 , mark^#(cons(X1, X2)) -> c_7(mark^#(X1), X2) 1148.69/298.79 , mark^#(first(X1, X2)) -> c_8(a__first^#(mark(X1), mark(X2))) 1148.69/298.79 , mark^#(from(X)) -> c_9(a__from^#(mark(X))) 1148.69/298.79 , a__from^#(X) -> c_10(mark^#(X), X) 1148.69/298.79 , a__from^#(X) -> c_11(X) } 1148.69/298.79 1148.69/298.79 and mark the set of starting terms. 1148.69/298.79 1148.69/298.79 We are left with following problem, upon which TcT provides the 1148.69/298.79 certificate MAYBE. 1148.69/298.79 1148.69/298.79 Strict DPs: 1148.69/298.79 { a__first^#(X1, X2) -> c_1(X1, X2) 1148.69/298.79 , a__first^#(0(), X) -> c_2() 1148.69/298.79 , a__first^#(s(X), cons(Y, Z)) -> c_3(mark^#(Y), X, Z) 1148.69/298.79 , mark^#(0()) -> c_4() 1148.69/298.79 , mark^#(nil()) -> c_5() 1148.69/298.79 , mark^#(s(X)) -> c_6(mark^#(X)) 1148.69/298.79 , mark^#(cons(X1, X2)) -> c_7(mark^#(X1), X2) 1148.69/298.79 , mark^#(first(X1, X2)) -> c_8(a__first^#(mark(X1), mark(X2))) 1148.69/298.79 , mark^#(from(X)) -> c_9(a__from^#(mark(X))) 1148.69/298.79 , a__from^#(X) -> c_10(mark^#(X), X) 1148.69/298.79 , a__from^#(X) -> c_11(X) } 1148.69/298.79 Strict Trs: 1148.69/298.79 { a__first(X1, X2) -> first(X1, X2) 1148.69/298.79 , a__first(0(), X) -> nil() 1148.69/298.79 , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)) 1148.69/298.79 , mark(0()) -> 0() 1148.69/298.79 , mark(nil()) -> nil() 1148.69/298.79 , mark(s(X)) -> s(mark(X)) 1148.69/298.79 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 1148.69/298.79 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1148.69/298.79 , mark(from(X)) -> a__from(mark(X)) 1148.69/298.79 , a__from(X) -> cons(mark(X), from(s(X))) 1148.69/298.79 , a__from(X) -> from(X) } 1148.69/298.79 Obligation: 1148.69/298.79 runtime complexity 1148.69/298.79 Answer: 1148.69/298.79 MAYBE 1148.69/298.79 1148.69/298.79 We estimate the number of application of {2,4,5} by applications of 1148.69/298.79 Pre({2,4,5}) = {1,3,6,7,8,10,11}. Here rules are labeled as 1148.69/298.79 follows: 1148.69/298.79 1148.69/298.79 DPs: 1148.69/298.79 { 1: a__first^#(X1, X2) -> c_1(X1, X2) 1148.69/298.79 , 2: a__first^#(0(), X) -> c_2() 1148.69/298.79 , 3: a__first^#(s(X), cons(Y, Z)) -> c_3(mark^#(Y), X, Z) 1148.69/298.79 , 4: mark^#(0()) -> c_4() 1148.69/298.79 , 5: mark^#(nil()) -> c_5() 1148.69/298.79 , 6: mark^#(s(X)) -> c_6(mark^#(X)) 1148.69/298.79 , 7: mark^#(cons(X1, X2)) -> c_7(mark^#(X1), X2) 1148.69/298.79 , 8: mark^#(first(X1, X2)) -> c_8(a__first^#(mark(X1), mark(X2))) 1148.69/298.79 , 9: mark^#(from(X)) -> c_9(a__from^#(mark(X))) 1148.69/298.79 , 10: a__from^#(X) -> c_10(mark^#(X), X) 1148.69/298.79 , 11: a__from^#(X) -> c_11(X) } 1148.69/298.79 1148.69/298.79 We are left with following problem, upon which TcT provides the 1148.69/298.79 certificate MAYBE. 1148.69/298.79 1148.69/298.79 Strict DPs: 1148.69/298.79 { a__first^#(X1, X2) -> c_1(X1, X2) 1148.69/298.79 , a__first^#(s(X), cons(Y, Z)) -> c_3(mark^#(Y), X, Z) 1148.69/298.79 , mark^#(s(X)) -> c_6(mark^#(X)) 1148.69/298.79 , mark^#(cons(X1, X2)) -> c_7(mark^#(X1), X2) 1148.69/298.79 , mark^#(first(X1, X2)) -> c_8(a__first^#(mark(X1), mark(X2))) 1148.69/298.79 , mark^#(from(X)) -> c_9(a__from^#(mark(X))) 1148.69/298.79 , a__from^#(X) -> c_10(mark^#(X), X) 1148.69/298.79 , a__from^#(X) -> c_11(X) } 1148.69/298.79 Strict Trs: 1148.69/298.79 { a__first(X1, X2) -> first(X1, X2) 1148.69/298.79 , a__first(0(), X) -> nil() 1148.69/298.79 , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)) 1148.69/298.79 , mark(0()) -> 0() 1148.69/298.79 , mark(nil()) -> nil() 1148.69/298.79 , mark(s(X)) -> s(mark(X)) 1148.69/298.79 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 1148.69/298.79 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1148.69/298.79 , mark(from(X)) -> a__from(mark(X)) 1148.69/298.79 , a__from(X) -> cons(mark(X), from(s(X))) 1148.69/298.79 , a__from(X) -> from(X) } 1148.69/298.79 Weak DPs: 1148.69/298.79 { a__first^#(0(), X) -> c_2() 1148.69/298.79 , mark^#(0()) -> c_4() 1148.69/298.79 , mark^#(nil()) -> c_5() } 1148.69/298.79 Obligation: 1148.69/298.79 runtime complexity 1148.69/298.79 Answer: 1148.69/298.79 MAYBE 1148.69/298.79 1148.69/298.79 Empty strict component of the problem is NOT empty. 1148.69/298.79 1148.69/298.79 1148.69/298.79 Arrrr.. 1149.75/299.53 EOF