MAYBE 703.53/297.02 MAYBE 703.53/297.02 703.53/297.02 We are left with following problem, upon which TcT provides the 703.53/297.02 certificate MAYBE. 703.53/297.02 703.53/297.02 Strict Trs: 703.53/297.02 { sort(l) -> st(0(), l) 703.53/297.02 , st(n, l) -> cond1(member(n, l), n, l) 703.53/297.02 , cond1(true(), n, l) -> cons(n, st(s(n), l)) 703.53/297.02 , cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l) 703.53/297.02 , member(n, cons(m, l)) -> or(equal(n, m), member(n, l)) 703.53/297.02 , member(n, nil()) -> false() 703.53/297.02 , cond2(true(), n, l) -> nil() 703.53/297.02 , cond2(false(), n, l) -> st(s(n), l) 703.53/297.02 , gt(0(), v) -> false() 703.53/297.02 , gt(s(u), 0()) -> true() 703.53/297.02 , gt(s(u), s(v)) -> gt(u, v) 703.53/297.02 , max(cons(u, l)) -> if(gt(u, max(l)), u, max(l)) 703.53/297.02 , max(nil()) -> 0() 703.53/297.02 , or(x, true()) -> true() 703.53/297.02 , or(x, false()) -> x 703.53/297.02 , equal(0(), 0()) -> true() 703.53/297.02 , equal(0(), s(y)) -> false() 703.53/297.02 , equal(s(x), 0()) -> false() 703.53/297.02 , equal(s(x), s(y)) -> equal(x, y) 703.53/297.02 , if(true(), u, v) -> u 703.53/297.02 , if(false(), u, v) -> v } 703.53/297.02 Obligation: 703.53/297.02 innermost runtime complexity 703.53/297.02 Answer: 703.53/297.02 MAYBE 703.53/297.02 703.53/297.02 None of the processors succeeded. 703.53/297.02 703.53/297.02 Details of failed attempt(s): 703.53/297.02 ----------------------------- 703.53/297.02 1) 'empty' failed due to the following reason: 703.53/297.02 703.53/297.02 Empty strict component of the problem is NOT empty. 703.53/297.02 703.53/297.02 2) 'Best' failed due to the following reason: 703.53/297.02 703.53/297.02 None of the processors succeeded. 703.53/297.02 703.53/297.02 Details of failed attempt(s): 703.53/297.02 ----------------------------- 703.53/297.02 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 703.53/297.02 following reason: 703.53/297.02 703.53/297.02 Computation stopped due to timeout after 297.0 seconds. 703.53/297.02 703.53/297.02 2) 'Best' failed due to the following reason: 703.53/297.02 703.53/297.02 None of the processors succeeded. 703.53/297.02 703.53/297.02 Details of failed attempt(s): 703.53/297.02 ----------------------------- 703.53/297.02 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 703.53/297.02 seconds)' failed due to the following reason: 703.53/297.02 703.53/297.02 Computation stopped due to timeout after 148.0 seconds. 703.53/297.02 703.53/297.02 2) 'Best' failed due to the following reason: 703.53/297.02 703.53/297.02 None of the processors succeeded. 703.53/297.02 703.53/297.02 Details of failed attempt(s): 703.53/297.02 ----------------------------- 703.53/297.02 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 703.53/297.02 to the following reason: 703.53/297.02 703.53/297.02 The input cannot be shown compatible 703.53/297.02 703.53/297.02 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 703.53/297.02 following reason: 703.53/297.02 703.53/297.02 The input cannot be shown compatible 703.53/297.02 703.53/297.02 703.53/297.02 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 703.53/297.02 failed due to the following reason: 703.53/297.02 703.53/297.02 None of the processors succeeded. 703.53/297.02 703.53/297.02 Details of failed attempt(s): 703.53/297.02 ----------------------------- 703.53/297.02 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 703.53/297.02 failed due to the following reason: 703.53/297.02 703.53/297.02 match-boundness of the problem could not be verified. 703.53/297.02 703.53/297.02 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 703.53/297.02 failed due to the following reason: 703.53/297.02 703.53/297.02 match-boundness of the problem could not be verified. 703.53/297.02 703.53/297.02 703.53/297.02 703.53/297.02 703.53/297.02 703.53/297.02 Arrrr.. 703.53/297.12 EOF