MAYBE 1184.98/297.20 MAYBE 1184.98/297.20 1184.98/297.20 We are left with following problem, upon which TcT provides the 1184.98/297.20 certificate MAYBE. 1184.98/297.20 1184.98/297.20 Strict Trs: 1184.98/297.20 { isEmpty(empty()) -> true() 1184.98/297.20 , isEmpty(node(l, x, r)) -> false() 1184.98/297.20 , left(empty()) -> empty() 1184.98/297.20 , left(node(l, x, r)) -> l 1184.98/297.20 , right(empty()) -> empty() 1184.98/297.20 , right(node(l, x, r)) -> r 1184.98/297.20 , elem(node(l, x, r)) -> x 1184.98/297.20 , append(nil(), x) -> cons(x, nil()) 1184.98/297.20 , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) 1184.98/297.20 , listify(n, xs) -> 1184.98/297.20 if(isEmpty(n), 1184.98/297.20 isEmpty(left(n)), 1184.98/297.20 right(n), 1184.98/297.20 node(left(left(n)), 1184.98/297.20 elem(left(n)), 1184.98/297.20 node(right(left(n)), elem(n), right(n))), 1184.98/297.20 xs, 1184.98/297.20 append(xs, n)) 1184.98/297.20 , if(true(), b, n, m, xs, ys) -> xs 1184.98/297.20 , if(false(), true(), n, m, xs, ys) -> listify(n, ys) 1184.98/297.20 , if(false(), false(), n, m, xs, ys) -> listify(m, xs) 1184.98/297.20 , toList(n) -> listify(n, nil()) } 1184.98/297.20 Obligation: 1184.98/297.20 runtime complexity 1184.98/297.20 Answer: 1184.98/297.20 MAYBE 1184.98/297.20 1184.98/297.20 None of the processors succeeded. 1184.98/297.20 1184.98/297.20 Details of failed attempt(s): 1184.98/297.20 ----------------------------- 1184.98/297.20 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1184.98/297.20 following reason: 1184.98/297.20 1184.98/297.20 Computation stopped due to timeout after 297.0 seconds. 1184.98/297.20 1184.98/297.20 2) 'Best' failed due to the following reason: 1184.98/297.20 1184.98/297.20 None of the processors succeeded. 1184.98/297.20 1184.98/297.20 Details of failed attempt(s): 1184.98/297.20 ----------------------------- 1184.98/297.20 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1184.98/297.20 seconds)' failed due to the following reason: 1184.98/297.20 1184.98/297.20 Computation stopped due to timeout after 148.0 seconds. 1184.98/297.20 1184.98/297.20 2) 'Best' failed due to the following reason: 1184.98/297.20 1184.98/297.20 None of the processors succeeded. 1184.98/297.20 1184.98/297.20 Details of failed attempt(s): 1184.98/297.20 ----------------------------- 1184.98/297.20 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1184.98/297.20 to the following reason: 1184.98/297.20 1184.98/297.20 The processor is inapplicable, reason: 1184.98/297.20 Processor only applicable for innermost runtime complexity analysis 1184.98/297.20 1184.98/297.20 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1184.98/297.20 following reason: 1184.98/297.20 1184.98/297.20 The processor is inapplicable, reason: 1184.98/297.20 Processor only applicable for innermost runtime complexity analysis 1184.98/297.20 1184.98/297.20 1184.98/297.20 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1184.98/297.20 failed due to the following reason: 1184.98/297.20 1184.98/297.20 None of the processors succeeded. 1184.98/297.20 1184.98/297.20 Details of failed attempt(s): 1184.98/297.20 ----------------------------- 1184.98/297.20 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1184.98/297.20 failed due to the following reason: 1184.98/297.20 1184.98/297.20 match-boundness of the problem could not be verified. 1184.98/297.20 1184.98/297.20 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1184.98/297.20 failed due to the following reason: 1184.98/297.20 1184.98/297.20 match-boundness of the problem could not be verified. 1184.98/297.20 1184.98/297.20 1184.98/297.20 1184.98/297.20 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1184.98/297.20 the following reason: 1184.98/297.20 1184.98/297.20 We add the following weak dependency pairs: 1184.98/297.20 1184.98/297.20 Strict DPs: 1184.98/297.20 { isEmpty^#(empty()) -> c_1() 1184.98/297.20 , isEmpty^#(node(l, x, r)) -> c_2() 1184.98/297.20 , left^#(empty()) -> c_3() 1184.98/297.20 , left^#(node(l, x, r)) -> c_4(l) 1184.98/297.20 , right^#(empty()) -> c_5() 1184.98/297.20 , right^#(node(l, x, r)) -> c_6(r) 1184.98/297.20 , elem^#(node(l, x, r)) -> c_7(x) 1184.98/297.20 , append^#(nil(), x) -> c_8(x) 1184.98/297.20 , append^#(cons(y(), ys), x) -> c_9(append^#(ys, x)) 1184.98/297.20 , listify^#(n, xs) -> 1184.98/297.20 c_10(if^#(isEmpty(n), 1184.98/297.20 isEmpty(left(n)), 1184.98/297.20 right(n), 1184.98/297.20 node(left(left(n)), 1184.98/297.20 elem(left(n)), 1184.98/297.20 node(right(left(n)), elem(n), right(n))), 1184.98/297.20 xs, 1184.98/297.20 append(xs, n))) 1184.98/297.20 , if^#(true(), b, n, m, xs, ys) -> c_11(xs) 1184.98/297.20 , if^#(false(), true(), n, m, xs, ys) -> c_12(listify^#(n, ys)) 1184.98/297.20 , if^#(false(), false(), n, m, xs, ys) -> c_13(listify^#(m, xs)) 1184.98/297.20 , toList^#(n) -> c_14(listify^#(n, nil())) } 1184.98/297.20 1184.98/297.20 and mark the set of starting terms. 1184.98/297.20 1184.98/297.20 We are left with following problem, upon which TcT provides the 1184.98/297.20 certificate MAYBE. 1184.98/297.20 1184.98/297.20 Strict DPs: 1184.98/297.20 { isEmpty^#(empty()) -> c_1() 1184.98/297.20 , isEmpty^#(node(l, x, r)) -> c_2() 1184.98/297.20 , left^#(empty()) -> c_3() 1184.98/297.20 , left^#(node(l, x, r)) -> c_4(l) 1184.98/297.20 , right^#(empty()) -> c_5() 1184.98/297.20 , right^#(node(l, x, r)) -> c_6(r) 1184.98/297.20 , elem^#(node(l, x, r)) -> c_7(x) 1184.98/297.20 , append^#(nil(), x) -> c_8(x) 1184.98/297.20 , append^#(cons(y(), ys), x) -> c_9(append^#(ys, x)) 1184.98/297.20 , listify^#(n, xs) -> 1184.98/297.20 c_10(if^#(isEmpty(n), 1184.98/297.20 isEmpty(left(n)), 1184.98/297.20 right(n), 1184.98/297.20 node(left(left(n)), 1184.98/297.20 elem(left(n)), 1184.98/297.20 node(right(left(n)), elem(n), right(n))), 1184.98/297.20 xs, 1184.98/297.20 append(xs, n))) 1184.98/297.20 , if^#(true(), b, n, m, xs, ys) -> c_11(xs) 1184.98/297.20 , if^#(false(), true(), n, m, xs, ys) -> c_12(listify^#(n, ys)) 1184.98/297.20 , if^#(false(), false(), n, m, xs, ys) -> c_13(listify^#(m, xs)) 1184.98/297.20 , toList^#(n) -> c_14(listify^#(n, nil())) } 1184.98/297.20 Strict Trs: 1184.98/297.20 { isEmpty(empty()) -> true() 1184.98/297.20 , isEmpty(node(l, x, r)) -> false() 1184.98/297.20 , left(empty()) -> empty() 1184.98/297.20 , left(node(l, x, r)) -> l 1184.98/297.20 , right(empty()) -> empty() 1184.98/297.20 , right(node(l, x, r)) -> r 1184.98/297.20 , elem(node(l, x, r)) -> x 1184.98/297.20 , append(nil(), x) -> cons(x, nil()) 1184.98/297.20 , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) 1184.98/297.20 , listify(n, xs) -> 1184.98/297.20 if(isEmpty(n), 1184.98/297.20 isEmpty(left(n)), 1184.98/297.20 right(n), 1184.98/297.20 node(left(left(n)), 1184.98/297.20 elem(left(n)), 1184.98/297.20 node(right(left(n)), elem(n), right(n))), 1184.98/297.20 xs, 1184.98/297.20 append(xs, n)) 1184.98/297.20 , if(true(), b, n, m, xs, ys) -> xs 1184.98/297.20 , if(false(), true(), n, m, xs, ys) -> listify(n, ys) 1184.98/297.20 , if(false(), false(), n, m, xs, ys) -> listify(m, xs) 1184.98/297.20 , toList(n) -> listify(n, nil()) } 1184.98/297.20 Obligation: 1184.98/297.20 runtime complexity 1184.98/297.20 Answer: 1184.98/297.20 MAYBE 1184.98/297.20 1184.98/297.20 We estimate the number of application of {1,2,3,5} by applications 1184.98/297.20 of Pre({1,2,3,5}) = {4,6,7,8,11}. Here rules are labeled as 1184.98/297.20 follows: 1184.98/297.20 1184.98/297.20 DPs: 1184.98/297.20 { 1: isEmpty^#(empty()) -> c_1() 1184.98/297.20 , 2: isEmpty^#(node(l, x, r)) -> c_2() 1184.98/297.20 , 3: left^#(empty()) -> c_3() 1184.98/297.20 , 4: left^#(node(l, x, r)) -> c_4(l) 1184.98/297.20 , 5: right^#(empty()) -> c_5() 1184.98/297.20 , 6: right^#(node(l, x, r)) -> c_6(r) 1184.98/297.20 , 7: elem^#(node(l, x, r)) -> c_7(x) 1184.98/297.20 , 8: append^#(nil(), x) -> c_8(x) 1184.98/297.20 , 9: append^#(cons(y(), ys), x) -> c_9(append^#(ys, x)) 1184.98/297.20 , 10: listify^#(n, xs) -> 1184.98/297.20 c_10(if^#(isEmpty(n), 1184.98/297.20 isEmpty(left(n)), 1184.98/297.20 right(n), 1184.98/297.20 node(left(left(n)), 1184.98/297.20 elem(left(n)), 1184.98/297.20 node(right(left(n)), elem(n), right(n))), 1184.98/297.20 xs, 1184.98/297.20 append(xs, n))) 1184.98/297.20 , 11: if^#(true(), b, n, m, xs, ys) -> c_11(xs) 1184.98/297.20 , 12: if^#(false(), true(), n, m, xs, ys) -> c_12(listify^#(n, ys)) 1184.98/297.20 , 13: if^#(false(), false(), n, m, xs, ys) -> 1184.98/297.20 c_13(listify^#(m, xs)) 1184.98/297.20 , 14: toList^#(n) -> c_14(listify^#(n, nil())) } 1184.98/297.20 1184.98/297.20 We are left with following problem, upon which TcT provides the 1184.98/297.20 certificate MAYBE. 1184.98/297.20 1184.98/297.20 Strict DPs: 1184.98/297.20 { left^#(node(l, x, r)) -> c_4(l) 1184.98/297.20 , right^#(node(l, x, r)) -> c_6(r) 1184.98/297.20 , elem^#(node(l, x, r)) -> c_7(x) 1184.98/297.20 , append^#(nil(), x) -> c_8(x) 1184.98/297.20 , append^#(cons(y(), ys), x) -> c_9(append^#(ys, x)) 1184.98/297.20 , listify^#(n, xs) -> 1184.98/297.20 c_10(if^#(isEmpty(n), 1184.98/297.20 isEmpty(left(n)), 1184.98/297.20 right(n), 1184.98/297.20 node(left(left(n)), 1184.98/297.20 elem(left(n)), 1184.98/297.20 node(right(left(n)), elem(n), right(n))), 1184.98/297.20 xs, 1184.98/297.20 append(xs, n))) 1184.98/297.20 , if^#(true(), b, n, m, xs, ys) -> c_11(xs) 1184.98/297.20 , if^#(false(), true(), n, m, xs, ys) -> c_12(listify^#(n, ys)) 1184.98/297.20 , if^#(false(), false(), n, m, xs, ys) -> c_13(listify^#(m, xs)) 1184.98/297.20 , toList^#(n) -> c_14(listify^#(n, nil())) } 1184.98/297.20 Strict Trs: 1184.98/297.20 { isEmpty(empty()) -> true() 1184.98/297.20 , isEmpty(node(l, x, r)) -> false() 1184.98/297.20 , left(empty()) -> empty() 1184.98/297.20 , left(node(l, x, r)) -> l 1184.98/297.20 , right(empty()) -> empty() 1184.98/297.20 , right(node(l, x, r)) -> r 1184.98/297.20 , elem(node(l, x, r)) -> x 1184.98/297.20 , append(nil(), x) -> cons(x, nil()) 1184.98/297.20 , append(cons(y(), ys), x) -> cons(y(), append(ys, x)) 1184.98/297.20 , listify(n, xs) -> 1184.98/297.20 if(isEmpty(n), 1184.98/297.20 isEmpty(left(n)), 1184.98/297.20 right(n), 1184.98/297.20 node(left(left(n)), 1184.98/297.20 elem(left(n)), 1184.98/297.20 node(right(left(n)), elem(n), right(n))), 1184.98/297.20 xs, 1184.98/297.20 append(xs, n)) 1184.98/297.20 , if(true(), b, n, m, xs, ys) -> xs 1184.98/297.20 , if(false(), true(), n, m, xs, ys) -> listify(n, ys) 1184.98/297.20 , if(false(), false(), n, m, xs, ys) -> listify(m, xs) 1184.98/297.20 , toList(n) -> listify(n, nil()) } 1184.98/297.20 Weak DPs: 1184.98/297.20 { isEmpty^#(empty()) -> c_1() 1184.98/297.20 , isEmpty^#(node(l, x, r)) -> c_2() 1184.98/297.20 , left^#(empty()) -> c_3() 1184.98/297.20 , right^#(empty()) -> c_5() } 1184.98/297.20 Obligation: 1184.98/297.20 runtime complexity 1184.98/297.20 Answer: 1184.98/297.20 MAYBE 1184.98/297.20 1184.98/297.20 Empty strict component of the problem is NOT empty. 1184.98/297.20 1184.98/297.20 1184.98/297.20 Arrrr.. 1185.98/298.27 EOF