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