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