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