MAYBE 861.97/297.03 MAYBE 861.97/297.03 861.97/297.03 We are left with following problem, upon which TcT provides the 861.97/297.03 certificate MAYBE. 861.97/297.03 861.97/297.03 Strict Trs: 861.97/297.03 { eq(0(), 0()) -> true() 861.97/297.03 , eq(0(), s(y)) -> false() 861.97/297.03 , eq(s(x), 0()) -> false() 861.97/297.03 , eq(s(x), s(y)) -> eq(x, y) 861.97/297.03 , lt(x, 0()) -> false() 861.97/297.03 , lt(0(), s(y)) -> true() 861.97/297.03 , lt(s(x), s(y)) -> lt(x, y) 861.97/297.03 , bin2s(nil()) -> 0() 861.97/297.03 , bin2s(cons(x, xs)) -> bin2ss(x, xs) 861.97/297.03 , bin2ss(x, nil()) -> x 861.97/297.03 , bin2ss(x, cons(0(), xs)) -> bin2ss(double(x), xs) 861.97/297.03 , bin2ss(x, cons(1(), xs)) -> bin2ss(s(double(x)), xs) 861.97/297.03 , half(0()) -> 0() 861.97/297.03 , half(s(0())) -> 0() 861.97/297.03 , half(s(s(x))) -> s(half(x)) 861.97/297.03 , log(0()) -> 0() 861.97/297.03 , log(s(0())) -> 0() 861.97/297.03 , log(s(s(x))) -> s(log(half(s(s(x))))) 861.97/297.03 , more(nil()) -> nil() 861.97/297.03 , more(cons(xs, ys)) -> 861.97/297.03 cons(cons(0(), xs), cons(cons(1(), xs), cons(xs, ys))) 861.97/297.03 , s2bin(x) -> s2bin1(x, 0(), cons(nil(), nil())) 861.97/297.03 , s2bin1(x, y, lists) -> if1(lt(y, log(x)), x, y, lists) 861.97/297.03 , if1(true(), x, y, lists) -> s2bin1(x, s(y), more(lists)) 861.97/297.03 , if1(false(), x, y, lists) -> s2bin2(x, lists) 861.97/297.03 , s2bin2(x, nil()) -> bug_list_not() 861.97/297.03 , s2bin2(x, cons(xs, ys)) -> if2(eq(x, bin2s(xs)), x, xs, ys) 861.97/297.03 , if2(true(), x, xs, ys) -> xs 861.97/297.03 , if2(false(), x, xs, ys) -> s2bin2(x, ys) } 861.97/297.03 Obligation: 861.97/297.03 runtime complexity 861.97/297.03 Answer: 861.97/297.03 MAYBE 861.97/297.03 861.97/297.03 None of the processors succeeded. 861.97/297.03 861.97/297.03 Details of failed attempt(s): 861.97/297.03 ----------------------------- 861.97/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 861.97/297.03 following reason: 861.97/297.03 861.97/297.03 Computation stopped due to timeout after 297.0 seconds. 861.97/297.03 861.97/297.03 2) 'Best' failed due to the following reason: 861.97/297.03 861.97/297.03 None of the processors succeeded. 861.97/297.03 861.97/297.03 Details of failed attempt(s): 861.97/297.03 ----------------------------- 861.97/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 861.97/297.03 seconds)' failed due to the following reason: 861.97/297.03 861.97/297.03 Computation stopped due to timeout after 148.0 seconds. 861.97/297.03 861.97/297.03 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 861.97/297.03 failed due to the following reason: 861.97/297.03 861.97/297.03 None of the processors succeeded. 861.97/297.03 861.97/297.03 Details of failed attempt(s): 861.97/297.03 ----------------------------- 861.97/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 861.97/297.03 failed due to the following reason: 861.97/297.03 861.97/297.03 match-boundness of the problem could not be verified. 861.97/297.03 861.97/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 861.97/297.03 failed due to the following reason: 861.97/297.03 861.97/297.03 match-boundness of the problem could not be verified. 861.97/297.03 861.97/297.03 861.97/297.03 3) 'Best' failed due to the following reason: 861.97/297.03 861.97/297.03 None of the processors succeeded. 861.97/297.03 861.97/297.03 Details of failed attempt(s): 861.97/297.03 ----------------------------- 861.97/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 861.97/297.03 following reason: 861.97/297.03 861.97/297.03 The processor is inapplicable, reason: 861.97/297.03 Processor only applicable for innermost runtime complexity analysis 861.97/297.03 861.97/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 861.97/297.03 to the following reason: 861.97/297.03 861.97/297.03 The processor is inapplicable, reason: 861.97/297.03 Processor only applicable for innermost runtime complexity analysis 861.97/297.03 861.97/297.03 861.97/297.03 861.97/297.03 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 861.97/297.03 the following reason: 861.97/297.03 861.97/297.03 We add the following weak dependency pairs: 861.97/297.03 861.97/297.03 Strict DPs: 861.97/297.03 { eq^#(0(), 0()) -> c_1() 861.97/297.03 , eq^#(0(), s(y)) -> c_2() 861.97/297.03 , eq^#(s(x), 0()) -> c_3() 861.97/297.03 , eq^#(s(x), s(y)) -> c_4(eq^#(x, y)) 861.97/297.03 , lt^#(x, 0()) -> c_5() 861.97/297.03 , lt^#(0(), s(y)) -> c_6() 861.97/297.03 , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) 861.97/297.03 , bin2s^#(nil()) -> c_8() 861.97/297.03 , bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs)) 861.97/297.03 , bin2ss^#(x, nil()) -> c_10(x) 861.97/297.03 , bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs)) 861.97/297.03 , bin2ss^#(x, cons(1(), xs)) -> c_12(bin2ss^#(s(double(x)), xs)) 861.97/297.03 , half^#(0()) -> c_13() 861.97/297.03 , half^#(s(0())) -> c_14() 861.97/297.03 , half^#(s(s(x))) -> c_15(half^#(x)) 861.97/297.03 , log^#(0()) -> c_16() 861.97/297.03 , log^#(s(0())) -> c_17() 861.97/297.03 , log^#(s(s(x))) -> c_18(log^#(half(s(s(x))))) 861.97/297.03 , more^#(nil()) -> c_19() 861.97/297.03 , more^#(cons(xs, ys)) -> c_20(xs, xs, xs, ys) 861.97/297.03 , s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil()))) 861.97/297.03 , s2bin1^#(x, y, lists) -> c_22(if1^#(lt(y, log(x)), x, y, lists)) 861.97/297.03 , if1^#(true(), x, y, lists) -> 861.97/297.03 c_23(s2bin1^#(x, s(y), more(lists))) 861.97/297.03 , if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists)) 861.97/297.03 , s2bin2^#(x, nil()) -> c_25() 861.97/297.03 , s2bin2^#(x, cons(xs, ys)) -> 861.97/297.03 c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys)) 861.97/297.03 , if2^#(true(), x, xs, ys) -> c_27(xs) 861.97/297.03 , if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) } 861.97/297.03 861.97/297.03 and mark the set of starting terms. 861.97/297.03 861.97/297.03 We are left with following problem, upon which TcT provides the 861.97/297.03 certificate MAYBE. 861.97/297.03 861.97/297.03 Strict DPs: 861.97/297.03 { eq^#(0(), 0()) -> c_1() 861.97/297.03 , eq^#(0(), s(y)) -> c_2() 861.97/297.03 , eq^#(s(x), 0()) -> c_3() 861.97/297.03 , eq^#(s(x), s(y)) -> c_4(eq^#(x, y)) 861.97/297.03 , lt^#(x, 0()) -> c_5() 861.97/297.03 , lt^#(0(), s(y)) -> c_6() 861.97/297.03 , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) 861.97/297.03 , bin2s^#(nil()) -> c_8() 861.97/297.03 , bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs)) 861.97/297.03 , bin2ss^#(x, nil()) -> c_10(x) 861.97/297.03 , bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs)) 861.97/297.03 , bin2ss^#(x, cons(1(), xs)) -> c_12(bin2ss^#(s(double(x)), xs)) 861.97/297.03 , half^#(0()) -> c_13() 861.97/297.03 , half^#(s(0())) -> c_14() 861.97/297.03 , half^#(s(s(x))) -> c_15(half^#(x)) 861.97/297.03 , log^#(0()) -> c_16() 861.97/297.03 , log^#(s(0())) -> c_17() 861.97/297.03 , log^#(s(s(x))) -> c_18(log^#(half(s(s(x))))) 861.97/297.03 , more^#(nil()) -> c_19() 861.97/297.03 , more^#(cons(xs, ys)) -> c_20(xs, xs, xs, ys) 861.97/297.03 , s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil()))) 861.97/297.03 , s2bin1^#(x, y, lists) -> c_22(if1^#(lt(y, log(x)), x, y, lists)) 861.97/297.03 , if1^#(true(), x, y, lists) -> 861.97/297.03 c_23(s2bin1^#(x, s(y), more(lists))) 861.97/297.03 , if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists)) 861.97/297.03 , s2bin2^#(x, nil()) -> c_25() 861.97/297.03 , s2bin2^#(x, cons(xs, ys)) -> 861.97/297.03 c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys)) 861.97/297.03 , if2^#(true(), x, xs, ys) -> c_27(xs) 861.97/297.03 , if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) } 861.97/297.03 Strict Trs: 861.97/297.03 { eq(0(), 0()) -> true() 861.97/297.03 , eq(0(), s(y)) -> false() 861.97/297.03 , eq(s(x), 0()) -> false() 861.97/297.03 , eq(s(x), s(y)) -> eq(x, y) 861.97/297.03 , lt(x, 0()) -> false() 861.97/297.03 , lt(0(), s(y)) -> true() 861.97/297.03 , lt(s(x), s(y)) -> lt(x, y) 861.97/297.03 , bin2s(nil()) -> 0() 861.97/297.03 , bin2s(cons(x, xs)) -> bin2ss(x, xs) 861.97/297.03 , bin2ss(x, nil()) -> x 861.97/297.03 , bin2ss(x, cons(0(), xs)) -> bin2ss(double(x), xs) 861.97/297.03 , bin2ss(x, cons(1(), xs)) -> bin2ss(s(double(x)), xs) 861.97/297.03 , half(0()) -> 0() 861.97/297.03 , half(s(0())) -> 0() 861.97/297.03 , half(s(s(x))) -> s(half(x)) 861.97/297.03 , log(0()) -> 0() 861.97/297.03 , log(s(0())) -> 0() 861.97/297.03 , log(s(s(x))) -> s(log(half(s(s(x))))) 861.97/297.03 , more(nil()) -> nil() 861.97/297.03 , more(cons(xs, ys)) -> 861.97/297.03 cons(cons(0(), xs), cons(cons(1(), xs), cons(xs, ys))) 861.97/297.03 , s2bin(x) -> s2bin1(x, 0(), cons(nil(), nil())) 861.97/297.03 , s2bin1(x, y, lists) -> if1(lt(y, log(x)), x, y, lists) 861.97/297.03 , if1(true(), x, y, lists) -> s2bin1(x, s(y), more(lists)) 861.97/297.03 , if1(false(), x, y, lists) -> s2bin2(x, lists) 861.97/297.03 , s2bin2(x, nil()) -> bug_list_not() 861.97/297.03 , s2bin2(x, cons(xs, ys)) -> if2(eq(x, bin2s(xs)), x, xs, ys) 861.97/297.03 , if2(true(), x, xs, ys) -> xs 861.97/297.03 , if2(false(), x, xs, ys) -> s2bin2(x, ys) } 861.97/297.03 Obligation: 861.97/297.03 runtime complexity 861.97/297.03 Answer: 861.97/297.03 MAYBE 861.97/297.03 861.97/297.03 We estimate the number of application of 861.97/297.03 {1,2,3,5,6,8,13,14,16,17,19,25} by applications of 861.97/297.03 Pre({1,2,3,5,6,8,13,14,16,17,19,25}) = {4,7,10,15,18,20,24,27,28}. 861.97/297.03 Here rules are labeled as follows: 861.97/297.03 861.97/297.03 DPs: 861.97/297.03 { 1: eq^#(0(), 0()) -> c_1() 861.97/297.03 , 2: eq^#(0(), s(y)) -> c_2() 861.97/297.03 , 3: eq^#(s(x), 0()) -> c_3() 861.97/297.03 , 4: eq^#(s(x), s(y)) -> c_4(eq^#(x, y)) 861.97/297.03 , 5: lt^#(x, 0()) -> c_5() 861.97/297.03 , 6: lt^#(0(), s(y)) -> c_6() 861.97/297.03 , 7: lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) 861.97/297.03 , 8: bin2s^#(nil()) -> c_8() 861.97/297.03 , 9: bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs)) 861.97/297.03 , 10: bin2ss^#(x, nil()) -> c_10(x) 861.97/297.03 , 11: bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs)) 861.97/297.03 , 12: bin2ss^#(x, cons(1(), xs)) -> 861.97/297.03 c_12(bin2ss^#(s(double(x)), xs)) 861.97/297.03 , 13: half^#(0()) -> c_13() 861.97/297.03 , 14: half^#(s(0())) -> c_14() 861.97/297.03 , 15: half^#(s(s(x))) -> c_15(half^#(x)) 861.97/297.03 , 16: log^#(0()) -> c_16() 861.97/297.03 , 17: log^#(s(0())) -> c_17() 861.97/297.03 , 18: log^#(s(s(x))) -> c_18(log^#(half(s(s(x))))) 861.97/297.03 , 19: more^#(nil()) -> c_19() 861.97/297.03 , 20: more^#(cons(xs, ys)) -> c_20(xs, xs, xs, ys) 861.97/297.03 , 21: s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil()))) 861.97/297.03 , 22: s2bin1^#(x, y, lists) -> 861.97/297.03 c_22(if1^#(lt(y, log(x)), x, y, lists)) 861.97/297.03 , 23: if1^#(true(), x, y, lists) -> 861.97/297.03 c_23(s2bin1^#(x, s(y), more(lists))) 861.97/297.03 , 24: if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists)) 861.97/297.03 , 25: s2bin2^#(x, nil()) -> c_25() 861.97/297.03 , 26: s2bin2^#(x, cons(xs, ys)) -> 861.97/297.03 c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys)) 861.97/297.03 , 27: if2^#(true(), x, xs, ys) -> c_27(xs) 861.97/297.03 , 28: if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) } 861.97/297.03 861.97/297.03 We are left with following problem, upon which TcT provides the 861.97/297.03 certificate MAYBE. 861.97/297.03 861.97/297.03 Strict DPs: 861.97/297.03 { eq^#(s(x), s(y)) -> c_4(eq^#(x, y)) 861.97/297.03 , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) 861.97/297.03 , bin2s^#(cons(x, xs)) -> c_9(bin2ss^#(x, xs)) 861.97/297.03 , bin2ss^#(x, nil()) -> c_10(x) 861.97/297.03 , bin2ss^#(x, cons(0(), xs)) -> c_11(bin2ss^#(double(x), xs)) 861.97/297.03 , bin2ss^#(x, cons(1(), xs)) -> c_12(bin2ss^#(s(double(x)), xs)) 861.97/297.03 , half^#(s(s(x))) -> c_15(half^#(x)) 861.97/297.03 , log^#(s(s(x))) -> c_18(log^#(half(s(s(x))))) 861.97/297.03 , more^#(cons(xs, ys)) -> c_20(xs, xs, xs, ys) 861.97/297.03 , s2bin^#(x) -> c_21(s2bin1^#(x, 0(), cons(nil(), nil()))) 861.97/297.03 , s2bin1^#(x, y, lists) -> c_22(if1^#(lt(y, log(x)), x, y, lists)) 861.97/297.03 , if1^#(true(), x, y, lists) -> 861.97/297.03 c_23(s2bin1^#(x, s(y), more(lists))) 861.97/297.03 , if1^#(false(), x, y, lists) -> c_24(s2bin2^#(x, lists)) 861.97/297.03 , s2bin2^#(x, cons(xs, ys)) -> 861.97/297.03 c_26(if2^#(eq(x, bin2s(xs)), x, xs, ys)) 861.97/297.03 , if2^#(true(), x, xs, ys) -> c_27(xs) 861.97/297.03 , if2^#(false(), x, xs, ys) -> c_28(s2bin2^#(x, ys)) } 861.97/297.03 Strict Trs: 861.97/297.03 { eq(0(), 0()) -> true() 861.97/297.03 , eq(0(), s(y)) -> false() 861.97/297.03 , eq(s(x), 0()) -> false() 861.97/297.03 , eq(s(x), s(y)) -> eq(x, y) 861.97/297.03 , lt(x, 0()) -> false() 861.97/297.03 , lt(0(), s(y)) -> true() 861.97/297.03 , lt(s(x), s(y)) -> lt(x, y) 861.97/297.03 , bin2s(nil()) -> 0() 861.97/297.03 , bin2s(cons(x, xs)) -> bin2ss(x, xs) 861.97/297.03 , bin2ss(x, nil()) -> x 861.97/297.03 , bin2ss(x, cons(0(), xs)) -> bin2ss(double(x), xs) 861.97/297.03 , bin2ss(x, cons(1(), xs)) -> bin2ss(s(double(x)), xs) 861.97/297.03 , half(0()) -> 0() 861.97/297.03 , half(s(0())) -> 0() 861.97/297.03 , half(s(s(x))) -> s(half(x)) 861.97/297.03 , log(0()) -> 0() 861.97/297.03 , log(s(0())) -> 0() 861.97/297.03 , log(s(s(x))) -> s(log(half(s(s(x))))) 861.97/297.03 , more(nil()) -> nil() 861.97/297.03 , more(cons(xs, ys)) -> 861.97/297.03 cons(cons(0(), xs), cons(cons(1(), xs), cons(xs, ys))) 861.97/297.03 , s2bin(x) -> s2bin1(x, 0(), cons(nil(), nil())) 861.97/297.03 , s2bin1(x, y, lists) -> if1(lt(y, log(x)), x, y, lists) 861.97/297.03 , if1(true(), x, y, lists) -> s2bin1(x, s(y), more(lists)) 861.97/297.03 , if1(false(), x, y, lists) -> s2bin2(x, lists) 861.97/297.03 , s2bin2(x, nil()) -> bug_list_not() 861.97/297.03 , s2bin2(x, cons(xs, ys)) -> if2(eq(x, bin2s(xs)), x, xs, ys) 861.97/297.03 , if2(true(), x, xs, ys) -> xs 861.97/297.03 , if2(false(), x, xs, ys) -> s2bin2(x, ys) } 861.97/297.03 Weak DPs: 861.97/297.03 { eq^#(0(), 0()) -> c_1() 861.97/297.03 , eq^#(0(), s(y)) -> c_2() 861.97/297.03 , eq^#(s(x), 0()) -> c_3() 861.97/297.03 , lt^#(x, 0()) -> c_5() 861.97/297.03 , lt^#(0(), s(y)) -> c_6() 861.97/297.03 , bin2s^#(nil()) -> c_8() 861.97/297.03 , half^#(0()) -> c_13() 861.97/297.03 , half^#(s(0())) -> c_14() 861.97/297.03 , log^#(0()) -> c_16() 861.97/297.03 , log^#(s(0())) -> c_17() 861.97/297.03 , more^#(nil()) -> c_19() 861.97/297.03 , s2bin2^#(x, nil()) -> c_25() } 861.97/297.03 Obligation: 861.97/297.03 runtime complexity 861.97/297.03 Answer: 861.97/297.03 MAYBE 861.97/297.03 861.97/297.03 Empty strict component of the problem is NOT empty. 861.97/297.03 861.97/297.03 861.97/297.03 Arrrr.. 862.09/297.17 EOF