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