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