MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , rev(x) -> if(x, eq(0(), length(x)), nil(), 0(), length(x)) , if(x, true(), z, c, l) -> z , if(x, false(), z, c, l) -> help(s(c), l, x, z) , length(nil()) -> 0() , length(cons(x, y)) -> s(length(y)) , help(c, l, cons(x, y), z) -> if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l) , append(nil(), y) -> y , append(cons(x, y), z) -> cons(x, append(y, z)) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { ge^#(x, 0()) -> c_1() , ge^#(0(), s(y)) -> c_2() , ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) , rev^#(x) -> c_4(if^#(x, eq(0(), length(x)), nil(), 0(), length(x))) , if^#(x, true(), z, c, l) -> c_5(z) , if^#(x, false(), z, c, l) -> c_6(help^#(s(c), l, x, z)) , help^#(c, l, cons(x, y), z) -> c_9(if^#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l)) , length^#(nil()) -> c_7() , length^#(cons(x, y)) -> c_8(length^#(y)) , append^#(nil(), y) -> c_10(y) , append^#(cons(x, y), z) -> c_11(x, append^#(y, z)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(x, 0()) -> c_1() , ge^#(0(), s(y)) -> c_2() , ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) , rev^#(x) -> c_4(if^#(x, eq(0(), length(x)), nil(), 0(), length(x))) , if^#(x, true(), z, c, l) -> c_5(z) , if^#(x, false(), z, c, l) -> c_6(help^#(s(c), l, x, z)) , help^#(c, l, cons(x, y), z) -> c_9(if^#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l)) , length^#(nil()) -> c_7() , length^#(cons(x, y)) -> c_8(length^#(y)) , append^#(nil(), y) -> c_10(y) , append^#(cons(x, y), z) -> c_11(x, append^#(y, z)) } Strict Trs: { ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , rev(x) -> if(x, eq(0(), length(x)), nil(), 0(), length(x)) , if(x, true(), z, c, l) -> z , if(x, false(), z, c, l) -> help(s(c), l, x, z) , length(nil()) -> 0() , length(cons(x, y)) -> s(length(y)) , help(c, l, cons(x, y), z) -> if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l) , append(nil(), y) -> y , append(cons(x, y), z) -> cons(x, append(y, z)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,4,8} by applications of Pre({1,2,4,8}) = {3,5,9,10,11}. Here rules are labeled as follows: DPs: { 1: ge^#(x, 0()) -> c_1() , 2: ge^#(0(), s(y)) -> c_2() , 3: ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) , 4: rev^#(x) -> c_4(if^#(x, eq(0(), length(x)), nil(), 0(), length(x))) , 5: if^#(x, true(), z, c, l) -> c_5(z) , 6: if^#(x, false(), z, c, l) -> c_6(help^#(s(c), l, x, z)) , 7: help^#(c, l, cons(x, y), z) -> c_9(if^#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l)) , 8: length^#(nil()) -> c_7() , 9: length^#(cons(x, y)) -> c_8(length^#(y)) , 10: append^#(nil(), y) -> c_10(y) , 11: append^#(cons(x, y), z) -> c_11(x, append^#(y, z)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) , if^#(x, true(), z, c, l) -> c_5(z) , if^#(x, false(), z, c, l) -> c_6(help^#(s(c), l, x, z)) , help^#(c, l, cons(x, y), z) -> c_9(if^#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l)) , length^#(cons(x, y)) -> c_8(length^#(y)) , append^#(nil(), y) -> c_10(y) , append^#(cons(x, y), z) -> c_11(x, append^#(y, z)) } Strict Trs: { ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , rev(x) -> if(x, eq(0(), length(x)), nil(), 0(), length(x)) , if(x, true(), z, c, l) -> z , if(x, false(), z, c, l) -> help(s(c), l, x, z) , length(nil()) -> 0() , length(cons(x, y)) -> s(length(y)) , help(c, l, cons(x, y), z) -> if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l) , append(nil(), y) -> y , append(cons(x, y), z) -> cons(x, append(y, z)) } Weak DPs: { ge^#(x, 0()) -> c_1() , ge^#(0(), s(y)) -> c_2() , rev^#(x) -> c_4(if^#(x, eq(0(), length(x)), nil(), 0(), length(x))) , length^#(nil()) -> c_7() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..