MAYBE 1036.97/297.03 MAYBE 1036.97/297.03 1036.97/297.03 We are left with following problem, upon which TcT provides the 1036.97/297.03 certificate MAYBE. 1036.97/297.03 1036.97/297.03 Strict Trs: 1036.97/297.03 { isEmpty(empty()) -> true() 1036.97/297.03 , isEmpty(node(l, x, r)) -> false() 1036.97/297.03 , left(empty()) -> empty() 1036.97/297.03 , left(node(l, x, r)) -> l 1036.97/297.03 , right(empty()) -> empty() 1036.97/297.03 , right(node(l, x, r)) -> r 1036.97/297.03 , elem(node(l, x, r)) -> x 1036.97/297.03 , append(nil(), x) -> cons(x, nil()) 1036.97/297.03 , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) 1036.97/297.03 , listify(n, xs) -> 1036.97/297.03 if(isEmpty(n), 1036.97/297.03 isEmpty(left(n)), 1036.97/297.03 right(n), 1036.97/297.03 node(left(left(n)), 1036.97/297.03 elem(left(n)), 1036.97/297.03 node(right(left(n)), elem(n), right(n))), 1036.97/297.03 xs, 1036.97/297.03 append(xs, n)) 1036.97/297.03 , if(true(), b, n, m, xs, ys) -> xs 1036.97/297.03 , if(false(), true(), n, m, xs, ys) -> listify(n, ys) 1036.97/297.03 , if(false(), false(), n, m, xs, ys) -> listify(m, xs) 1036.97/297.03 , toList(n) -> listify(n, nil()) } 1036.97/297.03 Obligation: 1036.97/297.03 innermost runtime complexity 1036.97/297.03 Answer: 1036.97/297.03 MAYBE 1036.97/297.03 1036.97/297.03 None of the processors succeeded. 1036.97/297.03 1036.97/297.03 Details of failed attempt(s): 1036.97/297.03 ----------------------------- 1036.97/297.03 1) 'empty' failed due to the following reason: 1036.97/297.03 1036.97/297.03 Empty strict component of the problem is NOT empty. 1036.97/297.03 1036.97/297.03 2) 'Best' failed due to the following reason: 1036.97/297.03 1036.97/297.03 None of the processors succeeded. 1036.97/297.03 1036.97/297.03 Details of failed attempt(s): 1036.97/297.03 ----------------------------- 1036.97/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1036.97/297.03 following reason: 1036.97/297.03 1036.97/297.03 Computation stopped due to timeout after 297.0 seconds. 1036.97/297.03 1036.97/297.03 2) 'Best' failed due to the following reason: 1036.97/297.03 1036.97/297.03 None of the processors succeeded. 1036.97/297.03 1036.97/297.03 Details of failed attempt(s): 1036.97/297.03 ----------------------------- 1036.97/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1036.97/297.03 seconds)' failed due to the following reason: 1036.97/297.03 1036.97/297.03 Computation stopped due to timeout after 148.0 seconds. 1036.97/297.03 1036.97/297.03 2) 'Best' failed due to the following reason: 1036.97/297.03 1036.97/297.03 None of the processors succeeded. 1036.97/297.03 1036.97/297.03 Details of failed attempt(s): 1036.97/297.03 ----------------------------- 1036.97/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1036.97/297.03 following reason: 1036.97/297.03 1036.97/297.03 The input cannot be shown compatible 1036.97/297.03 1036.97/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1036.97/297.03 to the following reason: 1036.97/297.03 1036.97/297.03 The input cannot be shown compatible 1036.97/297.03 1036.97/297.03 1036.97/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1036.97/297.03 failed due to the following reason: 1036.97/297.03 1036.97/297.03 None of the processors succeeded. 1036.97/297.03 1036.97/297.03 Details of failed attempt(s): 1036.97/297.03 ----------------------------- 1036.97/297.03 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1036.97/297.03 failed due to the following reason: 1036.97/297.03 1036.97/297.03 match-boundness of the problem could not be verified. 1036.97/297.03 1036.97/297.03 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 1036.97/297.03 failed due to the following reason: 1036.97/297.03 1036.97/297.03 match-boundness of the problem could not be verified. 1036.97/297.03 1036.97/297.03 1036.97/297.03 1036.97/297.03 1036.97/297.03 1036.97/297.03 Arrrr.. 1037.63/297.64 EOF