MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , bin2s(nil()) -> 0() , bin2s(cons(x, xs)) -> bin2ss(x, xs) , bin2ss(x, nil()) -> x , bin2ss(x, cons(0(), xs)) -> bin2ss(double(x), xs) , bin2ss(x, cons(1(), xs)) -> bin2ss(s(double(x)), xs) , half(0()) -> 0() , half(s(0())) -> 0() , half(s(s(x))) -> s(half(x)) , log(0()) -> 0() , log(s(0())) -> 0() , log(s(s(x))) -> s(log(half(s(s(x))))) , more(nil()) -> nil() , more(cons(xs, ys)) -> cons(cons(0(), xs), cons(cons(1(), xs), cons(xs, ys))) , s2bin(x) -> s2bin1(x, 0(), cons(nil(), nil())) , s2bin1(x, y, lists) -> if1(lt(y, log(x)), x, y, lists) , if1(true(), x, y, lists) -> s2bin1(x, s(y), more(lists)) , if1(false(), x, y, lists) -> s2bin2(x, lists) , s2bin2(x, nil()) -> bug_list_not() , s2bin2(x, cons(xs, ys)) -> if2(eq(x, bin2s(xs)), x, xs, ys) , if2(true(), x, xs, ys) -> xs , if2(false(), x, xs, ys) -> s2bin2(x, ys) } 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 minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-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: { eq^#(0(), 0()) -> c_1() , eq^#(0(), s(y)) -> c_2() , eq^#(s(x), 0()) -> c_3() , eq^#(s(x), s(y)) -> c_4(eq^#(x, y)) , lt^#(x, 0()) -> c_5() , lt^#(0(), s(y)) -> c_6() , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) , bin2s^#(nil()) -> c_8() , bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs)) , bin2ss^#(x, nil()) -> c_10(x) , bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs)) , bin2ss^#(x, cons(1(), xs)) -> c_12(bin2ss^#(s(double(x)), xs)) , half^#(0()) -> c_13() , half^#(s(0())) -> c_14() , half^#(s(s(x))) -> c_15(half^#(x)) , log^#(0()) -> c_16() , log^#(s(0())) -> c_17() , log^#(s(s(x))) -> c_18(log^#(half(s(s(x))))) , more^#(nil()) -> c_19() , more^#(cons(xs, ys)) -> c_20(xs, xs, xs, ys) , s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil()))) , s2bin1^#(x, y, lists) -> c_22(if1^#(lt(y, log(x)), x, y, lists)) , if1^#(true(), x, y, lists) -> c_23(s2bin1^#(x, s(y), more(lists))) , if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists)) , s2bin2^#(x, nil()) -> c_25() , s2bin2^#(x, cons(xs, ys)) -> c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys)) , if2^#(true(), x, xs, ys) -> c_27(xs) , if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { eq^#(0(), 0()) -> c_1() , eq^#(0(), s(y)) -> c_2() , eq^#(s(x), 0()) -> c_3() , eq^#(s(x), s(y)) -> c_4(eq^#(x, y)) , lt^#(x, 0()) -> c_5() , lt^#(0(), s(y)) -> c_6() , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) , bin2s^#(nil()) -> c_8() , bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs)) , bin2ss^#(x, nil()) -> c_10(x) , bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs)) , bin2ss^#(x, cons(1(), xs)) -> c_12(bin2ss^#(s(double(x)), xs)) , half^#(0()) -> c_13() , half^#(s(0())) -> c_14() , half^#(s(s(x))) -> c_15(half^#(x)) , log^#(0()) -> c_16() , log^#(s(0())) -> c_17() , log^#(s(s(x))) -> c_18(log^#(half(s(s(x))))) , more^#(nil()) -> c_19() , more^#(cons(xs, ys)) -> c_20(xs, xs, xs, ys) , s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil()))) , s2bin1^#(x, y, lists) -> c_22(if1^#(lt(y, log(x)), x, y, lists)) , if1^#(true(), x, y, lists) -> c_23(s2bin1^#(x, s(y), more(lists))) , if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists)) , s2bin2^#(x, nil()) -> c_25() , s2bin2^#(x, cons(xs, ys)) -> c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys)) , if2^#(true(), x, xs, ys) -> c_27(xs) , if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) } Strict Trs: { eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , bin2s(nil()) -> 0() , bin2s(cons(x, xs)) -> bin2ss(x, xs) , bin2ss(x, nil()) -> x , bin2ss(x, cons(0(), xs)) -> bin2ss(double(x), xs) , bin2ss(x, cons(1(), xs)) -> bin2ss(s(double(x)), xs) , half(0()) -> 0() , half(s(0())) -> 0() , half(s(s(x))) -> s(half(x)) , log(0()) -> 0() , log(s(0())) -> 0() , log(s(s(x))) -> s(log(half(s(s(x))))) , more(nil()) -> nil() , more(cons(xs, ys)) -> cons(cons(0(), xs), cons(cons(1(), xs), cons(xs, ys))) , s2bin(x) -> s2bin1(x, 0(), cons(nil(), nil())) , s2bin1(x, y, lists) -> if1(lt(y, log(x)), x, y, lists) , if1(true(), x, y, lists) -> s2bin1(x, s(y), more(lists)) , if1(false(), x, y, lists) -> s2bin2(x, lists) , s2bin2(x, nil()) -> bug_list_not() , s2bin2(x, cons(xs, ys)) -> if2(eq(x, bin2s(xs)), x, xs, ys) , if2(true(), x, xs, ys) -> xs , if2(false(), x, xs, ys) -> s2bin2(x, ys) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,5,6,8,13,14,16,17,19,25} by applications of Pre({1,2,3,5,6,8,13,14,16,17,19,25}) = {4,7,10,15,18,20,24,27,28}. Here rules are labeled as follows: DPs: { 1: eq^#(0(), 0()) -> c_1() , 2: eq^#(0(), s(y)) -> c_2() , 3: eq^#(s(x), 0()) -> c_3() , 4: eq^#(s(x), s(y)) -> c_4(eq^#(x, y)) , 5: lt^#(x, 0()) -> c_5() , 6: lt^#(0(), s(y)) -> c_6() , 7: lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) , 8: bin2s^#(nil()) -> c_8() , 9: bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs)) , 10: bin2ss^#(x, nil()) -> c_10(x) , 11: bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs)) , 12: bin2ss^#(x, cons(1(), xs)) -> c_12(bin2ss^#(s(double(x)), xs)) , 13: half^#(0()) -> c_13() , 14: half^#(s(0())) -> c_14() , 15: half^#(s(s(x))) -> c_15(half^#(x)) , 16: log^#(0()) -> c_16() , 17: log^#(s(0())) -> c_17() , 18: log^#(s(s(x))) -> c_18(log^#(half(s(s(x))))) , 19: more^#(nil()) -> c_19() , 20: more^#(cons(xs, ys)) -> c_20(xs, xs, xs, ys) , 21: s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil()))) , 22: s2bin1^#(x, y, lists) -> c_22(if1^#(lt(y, log(x)), x, y, lists)) , 23: if1^#(true(), x, y, lists) -> c_23(s2bin1^#(x, s(y), more(lists))) , 24: if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists)) , 25: s2bin2^#(x, nil()) -> c_25() , 26: s2bin2^#(x, cons(xs, ys)) -> c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys)) , 27: if2^#(true(), x, xs, ys) -> c_27(xs) , 28: if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { eq^#(s(x), s(y)) -> c_4(eq^#(x, y)) , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) , bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs)) , bin2ss^#(x, nil()) -> c_10(x) , bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs)) , bin2ss^#(x, cons(1(), xs)) -> c_12(bin2ss^#(s(double(x)), xs)) , half^#(s(s(x))) -> c_15(half^#(x)) , log^#(s(s(x))) -> c_18(log^#(half(s(s(x))))) , more^#(cons(xs, ys)) -> c_20(xs, xs, xs, ys) , s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil()))) , s2bin1^#(x, y, lists) -> c_22(if1^#(lt(y, log(x)), x, y, lists)) , if1^#(true(), x, y, lists) -> c_23(s2bin1^#(x, s(y), more(lists))) , if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists)) , s2bin2^#(x, cons(xs, ys)) -> c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys)) , if2^#(true(), x, xs, ys) -> c_27(xs) , if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) } Strict Trs: { eq(0(), 0()) -> true() , eq(0(), s(y)) -> false() , eq(s(x), 0()) -> false() , eq(s(x), s(y)) -> eq(x, y) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , bin2s(nil()) -> 0() , bin2s(cons(x, xs)) -> bin2ss(x, xs) , bin2ss(x, nil()) -> x , bin2ss(x, cons(0(), xs)) -> bin2ss(double(x), xs) , bin2ss(x, cons(1(), xs)) -> bin2ss(s(double(x)), xs) , half(0()) -> 0() , half(s(0())) -> 0() , half(s(s(x))) -> s(half(x)) , log(0()) -> 0() , log(s(0())) -> 0() , log(s(s(x))) -> s(log(half(s(s(x))))) , more(nil()) -> nil() , more(cons(xs, ys)) -> cons(cons(0(), xs), cons(cons(1(), xs), cons(xs, ys))) , s2bin(x) -> s2bin1(x, 0(), cons(nil(), nil())) , s2bin1(x, y, lists) -> if1(lt(y, log(x)), x, y, lists) , if1(true(), x, y, lists) -> s2bin1(x, s(y), more(lists)) , if1(false(), x, y, lists) -> s2bin2(x, lists) , s2bin2(x, nil()) -> bug_list_not() , s2bin2(x, cons(xs, ys)) -> if2(eq(x, bin2s(xs)), x, xs, ys) , if2(true(), x, xs, ys) -> xs , if2(false(), x, xs, ys) -> s2bin2(x, ys) } Weak DPs: { eq^#(0(), 0()) -> c_1() , eq^#(0(), s(y)) -> c_2() , eq^#(s(x), 0()) -> c_3() , lt^#(x, 0()) -> c_5() , lt^#(0(), s(y)) -> c_6() , bin2s^#(nil()) -> c_8() , half^#(0()) -> c_13() , half^#(s(0())) -> c_14() , log^#(0()) -> c_16() , log^#(s(0())) -> c_17() , more^#(nil()) -> c_19() , s2bin2^#(x, nil()) -> c_25() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..