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