MAYBE 915.41/297.03 MAYBE 915.41/297.03 915.41/297.03 We are left with following problem, upon which TcT provides the 915.41/297.03 certificate MAYBE. 915.41/297.03 915.41/297.03 Strict Trs: 915.41/297.03 { ge(x, 0()) -> true() 915.41/297.03 , ge(0(), s(y)) -> false() 915.41/297.03 , ge(s(x), s(y)) -> ge(x, y) 915.41/297.03 , rev(x) -> if(x, eq(0(), length(x)), nil(), 0(), length(x)) 915.41/297.03 , if(x, true(), z, c, l) -> z 915.41/297.03 , if(x, false(), z, c, l) -> help(s(c), l, x, z) 915.41/297.03 , length(nil()) -> 0() 915.41/297.03 , length(cons(x, y)) -> s(length(y)) 915.41/297.03 , help(c, l, cons(x, y), z) -> 915.41/297.03 if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l) 915.41/297.03 , append(nil(), y) -> y 915.41/297.03 , append(cons(x, y), z) -> cons(x, append(y, z)) } 915.41/297.03 Obligation: 915.41/297.03 innermost runtime complexity 915.41/297.03 Answer: 915.41/297.03 MAYBE 915.41/297.03 915.41/297.03 None of the processors succeeded. 915.41/297.03 915.41/297.03 Details of failed attempt(s): 915.41/297.03 ----------------------------- 915.41/297.03 1) 'empty' failed due to the following reason: 915.41/297.03 915.41/297.03 Empty strict component of the problem is NOT empty. 915.41/297.03 915.41/297.03 2) 'Best' failed due to the following reason: 915.41/297.03 915.41/297.03 None of the processors succeeded. 915.41/297.03 915.41/297.03 Details of failed attempt(s): 915.41/297.03 ----------------------------- 915.41/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 915.41/297.03 following reason: 915.41/297.03 915.41/297.03 Computation stopped due to timeout after 297.0 seconds. 915.41/297.03 915.41/297.03 2) 'Best' failed due to the following reason: 915.41/297.03 915.41/297.03 None of the processors succeeded. 915.41/297.03 915.41/297.03 Details of failed attempt(s): 915.41/297.03 ----------------------------- 915.41/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 915.41/297.03 seconds)' failed due to the following reason: 915.41/297.03 915.41/297.03 Computation stopped due to timeout after 148.0 seconds. 915.41/297.03 915.41/297.03 2) 'Best' failed due to the following reason: 915.41/297.03 915.41/297.03 None of the processors succeeded. 915.41/297.03 915.41/297.03 Details of failed attempt(s): 915.41/297.03 ----------------------------- 915.41/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 915.41/297.03 following reason: 915.41/297.03 915.41/297.03 The input cannot be shown compatible 915.41/297.03 915.41/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 915.41/297.03 to the following reason: 915.41/297.03 915.41/297.03 The input cannot be shown compatible 915.41/297.03 915.41/297.03 915.41/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 915.41/297.03 failed due to the following reason: 915.41/297.03 915.41/297.03 None of the processors succeeded. 915.41/297.03 915.41/297.03 Details of failed attempt(s): 915.41/297.03 ----------------------------- 915.41/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 915.41/297.03 failed due to the following reason: 915.41/297.03 915.41/297.03 match-boundness of the problem could not be verified. 915.41/297.03 915.41/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 915.41/297.03 failed due to the following reason: 915.41/297.03 915.41/297.03 match-boundness of the problem could not be verified. 915.41/297.03 915.41/297.03 915.41/297.03 915.41/297.03 915.41/297.03 915.41/297.03 Arrrr.. 915.72/297.32 EOF