MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { car(cons(x, l)) -> x , cddr(cons(x, cons(y, l))) -> l , cddr(cons(x, nil())) -> nil() , cddr(nil()) -> nil() , cadr(cons(x, cons(y, l))) -> y , isZero(0()) -> true() , isZero(s(x)) -> false() , plus(x, y) -> ifplus(isZero(x), x, y) , ifplus(true(), x, y) -> y , ifplus(false(), x, y) -> s(plus(p(x), y)) , p(0()) -> 0() , p(s(x)) -> x , times(x, y) -> iftimes(isZero(x), x, y) , iftimes(true(), x, y) -> 0() , iftimes(false(), x, y) -> plus(y, times(p(x), y)) , shorter(cons(x, l), 0()) -> false() , shorter(cons(x, l), s(y)) -> shorter(l, y) , shorter(nil(), y) -> true() , prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l) , if(true(), b, l) -> s(0()) , if(false(), b, l) -> if2(b, l) , if2(true(), l) -> car(l) , if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l))) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { car^#(cons(x, l)) -> c_1(x) , cddr^#(cons(x, cons(y, l))) -> c_2(l) , cddr^#(cons(x, nil())) -> c_3() , cddr^#(nil()) -> c_4() , cadr^#(cons(x, cons(y, l))) -> c_5(y) , isZero^#(0()) -> c_6() , isZero^#(s(x)) -> c_7() , plus^#(x, y) -> c_8(ifplus^#(isZero(x), x, y)) , ifplus^#(true(), x, y) -> c_9(y) , ifplus^#(false(), x, y) -> c_10(plus^#(p(x), y)) , p^#(0()) -> c_11() , p^#(s(x)) -> c_12(x) , times^#(x, y) -> c_13(iftimes^#(isZero(x), x, y)) , iftimes^#(true(), x, y) -> c_14() , iftimes^#(false(), x, y) -> c_15(plus^#(y, times(p(x), y))) , shorter^#(cons(x, l), 0()) -> c_16() , shorter^#(cons(x, l), s(y)) -> c_17(shorter^#(l, y)) , shorter^#(nil(), y) -> c_18() , prod^#(l) -> c_19(if^#(shorter(l, 0()), shorter(l, s(0())), l)) , if^#(true(), b, l) -> c_20() , if^#(false(), b, l) -> c_21(if2^#(b, l)) , if2^#(true(), l) -> c_22(car^#(l)) , if2^#(false(), l) -> c_23(prod^#(cons(times(car(l), cadr(l)), cddr(l)))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { car^#(cons(x, l)) -> c_1(x) , cddr^#(cons(x, cons(y, l))) -> c_2(l) , cddr^#(cons(x, nil())) -> c_3() , cddr^#(nil()) -> c_4() , cadr^#(cons(x, cons(y, l))) -> c_5(y) , isZero^#(0()) -> c_6() , isZero^#(s(x)) -> c_7() , plus^#(x, y) -> c_8(ifplus^#(isZero(x), x, y)) , ifplus^#(true(), x, y) -> c_9(y) , ifplus^#(false(), x, y) -> c_10(plus^#(p(x), y)) , p^#(0()) -> c_11() , p^#(s(x)) -> c_12(x) , times^#(x, y) -> c_13(iftimes^#(isZero(x), x, y)) , iftimes^#(true(), x, y) -> c_14() , iftimes^#(false(), x, y) -> c_15(plus^#(y, times(p(x), y))) , shorter^#(cons(x, l), 0()) -> c_16() , shorter^#(cons(x, l), s(y)) -> c_17(shorter^#(l, y)) , shorter^#(nil(), y) -> c_18() , prod^#(l) -> c_19(if^#(shorter(l, 0()), shorter(l, s(0())), l)) , if^#(true(), b, l) -> c_20() , if^#(false(), b, l) -> c_21(if2^#(b, l)) , if2^#(true(), l) -> c_22(car^#(l)) , if2^#(false(), l) -> c_23(prod^#(cons(times(car(l), cadr(l)), cddr(l)))) } Strict Trs: { car(cons(x, l)) -> x , cddr(cons(x, cons(y, l))) -> l , cddr(cons(x, nil())) -> nil() , cddr(nil()) -> nil() , cadr(cons(x, cons(y, l))) -> y , isZero(0()) -> true() , isZero(s(x)) -> false() , plus(x, y) -> ifplus(isZero(x), x, y) , ifplus(true(), x, y) -> y , ifplus(false(), x, y) -> s(plus(p(x), y)) , p(0()) -> 0() , p(s(x)) -> x , times(x, y) -> iftimes(isZero(x), x, y) , iftimes(true(), x, y) -> 0() , iftimes(false(), x, y) -> plus(y, times(p(x), y)) , shorter(cons(x, l), 0()) -> false() , shorter(cons(x, l), s(y)) -> shorter(l, y) , shorter(nil(), y) -> true() , prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l) , if(true(), b, l) -> s(0()) , if(false(), b, l) -> if2(b, l) , if2(true(), l) -> car(l) , if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l))) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {3,4,6,7,11,14,16,18,20} by applications of Pre({3,4,6,7,11,14,16,18,20}) = {1,2,5,9,12,13,17,19}. Here rules are labeled as follows: DPs: { 1: car^#(cons(x, l)) -> c_1(x) , 2: cddr^#(cons(x, cons(y, l))) -> c_2(l) , 3: cddr^#(cons(x, nil())) -> c_3() , 4: cddr^#(nil()) -> c_4() , 5: cadr^#(cons(x, cons(y, l))) -> c_5(y) , 6: isZero^#(0()) -> c_6() , 7: isZero^#(s(x)) -> c_7() , 8: plus^#(x, y) -> c_8(ifplus^#(isZero(x), x, y)) , 9: ifplus^#(true(), x, y) -> c_9(y) , 10: ifplus^#(false(), x, y) -> c_10(plus^#(p(x), y)) , 11: p^#(0()) -> c_11() , 12: p^#(s(x)) -> c_12(x) , 13: times^#(x, y) -> c_13(iftimes^#(isZero(x), x, y)) , 14: iftimes^#(true(), x, y) -> c_14() , 15: iftimes^#(false(), x, y) -> c_15(plus^#(y, times(p(x), y))) , 16: shorter^#(cons(x, l), 0()) -> c_16() , 17: shorter^#(cons(x, l), s(y)) -> c_17(shorter^#(l, y)) , 18: shorter^#(nil(), y) -> c_18() , 19: prod^#(l) -> c_19(if^#(shorter(l, 0()), shorter(l, s(0())), l)) , 20: if^#(true(), b, l) -> c_20() , 21: if^#(false(), b, l) -> c_21(if2^#(b, l)) , 22: if2^#(true(), l) -> c_22(car^#(l)) , 23: if2^#(false(), l) -> c_23(prod^#(cons(times(car(l), cadr(l)), cddr(l)))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { car^#(cons(x, l)) -> c_1(x) , cddr^#(cons(x, cons(y, l))) -> c_2(l) , cadr^#(cons(x, cons(y, l))) -> c_5(y) , plus^#(x, y) -> c_8(ifplus^#(isZero(x), x, y)) , ifplus^#(true(), x, y) -> c_9(y) , ifplus^#(false(), x, y) -> c_10(plus^#(p(x), y)) , p^#(s(x)) -> c_12(x) , times^#(x, y) -> c_13(iftimes^#(isZero(x), x, y)) , iftimes^#(false(), x, y) -> c_15(plus^#(y, times(p(x), y))) , shorter^#(cons(x, l), s(y)) -> c_17(shorter^#(l, y)) , prod^#(l) -> c_19(if^#(shorter(l, 0()), shorter(l, s(0())), l)) , if^#(false(), b, l) -> c_21(if2^#(b, l)) , if2^#(true(), l) -> c_22(car^#(l)) , if2^#(false(), l) -> c_23(prod^#(cons(times(car(l), cadr(l)), cddr(l)))) } Strict Trs: { car(cons(x, l)) -> x , cddr(cons(x, cons(y, l))) -> l , cddr(cons(x, nil())) -> nil() , cddr(nil()) -> nil() , cadr(cons(x, cons(y, l))) -> y , isZero(0()) -> true() , isZero(s(x)) -> false() , plus(x, y) -> ifplus(isZero(x), x, y) , ifplus(true(), x, y) -> y , ifplus(false(), x, y) -> s(plus(p(x), y)) , p(0()) -> 0() , p(s(x)) -> x , times(x, y) -> iftimes(isZero(x), x, y) , iftimes(true(), x, y) -> 0() , iftimes(false(), x, y) -> plus(y, times(p(x), y)) , shorter(cons(x, l), 0()) -> false() , shorter(cons(x, l), s(y)) -> shorter(l, y) , shorter(nil(), y) -> true() , prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l) , if(true(), b, l) -> s(0()) , if(false(), b, l) -> if2(b, l) , if2(true(), l) -> car(l) , if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l))) } Weak DPs: { cddr^#(cons(x, nil())) -> c_3() , cddr^#(nil()) -> c_4() , isZero^#(0()) -> c_6() , isZero^#(s(x)) -> c_7() , p^#(0()) -> c_11() , iftimes^#(true(), x, y) -> c_14() , shorter^#(cons(x, l), 0()) -> c_16() , shorter^#(nil(), y) -> c_18() , if^#(true(), b, l) -> c_20() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..