MAYBE 738.64/297.04 MAYBE 738.64/297.04 738.64/297.04 We are left with following problem, upon which TcT provides the 738.64/297.04 certificate MAYBE. 738.64/297.04 738.64/297.04 Strict Trs: 738.64/297.04 { 0(#()) -> #() 738.64/297.04 , +(x, #()) -> x 738.64/297.04 , +(0(x), 0(y)) -> 0(+(x, y)) 738.64/297.04 , +(0(x), 1(y)) -> 1(+(x, y)) 738.64/297.04 , +(0(x), j(y)) -> j(+(x, y)) 738.64/297.04 , +(#(), x) -> x 738.64/297.04 , +(+(x, y), z) -> +(x, +(y, z)) 738.64/297.04 , +(1(x), 0(y)) -> 1(+(x, y)) 738.64/297.04 , +(1(x), 1(y)) -> j(+(+(x, y), 1(#()))) 738.64/297.04 , +(1(x), j(y)) -> 0(+(x, y)) 738.64/297.04 , +(j(x), 0(y)) -> j(+(x, y)) 738.64/297.04 , +(j(x), 1(y)) -> 0(+(x, y)) 738.64/297.04 , +(j(x), j(y)) -> 1(+(+(x, y), j(#()))) 738.64/297.04 , opp(0(x)) -> 0(opp(x)) 738.64/297.04 , opp(#()) -> #() 738.64/297.04 , opp(1(x)) -> j(opp(x)) 738.64/297.04 , opp(j(x)) -> 1(opp(x)) 738.64/297.04 , -(x, y) -> +(x, opp(y)) 738.64/297.04 , *(0(x), y) -> 0(*(x, y)) 738.64/297.04 , *(#(), x) -> #() 738.64/297.04 , *(1(x), y) -> +(0(*(x, y)), y) 738.64/297.04 , *(j(x), y) -> -(0(*(x, y)), y) 738.64/297.04 , *(*(x, y), z) -> *(x, *(y, z)) } 738.64/297.04 Obligation: 738.64/297.04 runtime complexity 738.64/297.04 Answer: 738.64/297.04 MAYBE 738.64/297.04 738.64/297.04 None of the processors succeeded. 738.64/297.04 738.64/297.04 Details of failed attempt(s): 738.64/297.04 ----------------------------- 738.64/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 738.64/297.04 following reason: 738.64/297.04 738.64/297.04 Computation stopped due to timeout after 297.0 seconds. 738.64/297.04 738.64/297.04 2) 'Best' failed due to the following reason: 738.64/297.04 738.64/297.04 None of the processors succeeded. 738.64/297.04 738.64/297.04 Details of failed attempt(s): 738.64/297.04 ----------------------------- 738.64/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 738.64/297.04 seconds)' failed due to the following reason: 738.64/297.04 738.64/297.04 Computation stopped due to timeout after 148.0 seconds. 738.64/297.04 738.64/297.04 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 738.64/297.04 failed due to the following reason: 738.64/297.04 738.64/297.04 None of the processors succeeded. 738.64/297.04 738.64/297.04 Details of failed attempt(s): 738.64/297.04 ----------------------------- 738.64/297.04 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 738.64/297.04 failed due to the following reason: 738.64/297.04 738.64/297.04 match-boundness of the problem could not be verified. 738.64/297.04 738.64/297.04 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 738.64/297.04 failed due to the following reason: 738.64/297.04 738.64/297.04 match-boundness of the problem could not be verified. 738.64/297.04 738.64/297.04 738.64/297.04 3) 'Best' failed due to the following reason: 738.64/297.04 738.64/297.04 None of the processors succeeded. 738.64/297.04 738.64/297.04 Details of failed attempt(s): 738.64/297.04 ----------------------------- 738.64/297.04 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 738.64/297.04 following reason: 738.64/297.04 738.64/297.04 The processor is inapplicable, reason: 738.64/297.04 Processor only applicable for innermost runtime complexity analysis 738.64/297.04 738.64/297.04 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 738.64/297.04 to the following reason: 738.64/297.04 738.64/297.04 The processor is inapplicable, reason: 738.64/297.04 Processor only applicable for innermost runtime complexity analysis 738.64/297.04 738.64/297.04 738.64/297.04 738.64/297.04 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 738.64/297.04 the following reason: 738.64/297.04 738.64/297.04 We add the following weak dependency pairs: 738.64/297.04 738.64/297.04 Strict DPs: 738.64/297.04 { 0^#(#()) -> c_1() 738.64/297.04 , +^#(x, #()) -> c_2(x) 738.64/297.04 , +^#(0(x), 0(y)) -> c_3(0^#(+(x, y))) 738.64/297.04 , +^#(0(x), 1(y)) -> c_4(+^#(x, y)) 738.64/297.04 , +^#(0(x), j(y)) -> c_5(+^#(x, y)) 738.64/297.04 , +^#(#(), x) -> c_6(x) 738.64/297.04 , +^#(+(x, y), z) -> c_7(+^#(x, +(y, z))) 738.64/297.04 , +^#(1(x), 0(y)) -> c_8(+^#(x, y)) 738.64/297.04 , +^#(1(x), 1(y)) -> c_9(+^#(+(x, y), 1(#()))) 738.64/297.04 , +^#(1(x), j(y)) -> c_10(0^#(+(x, y))) 738.64/297.04 , +^#(j(x), 0(y)) -> c_11(+^#(x, y)) 738.64/297.04 , +^#(j(x), 1(y)) -> c_12(0^#(+(x, y))) 738.64/297.04 , +^#(j(x), j(y)) -> c_13(+^#(+(x, y), j(#()))) 738.64/297.04 , opp^#(0(x)) -> c_14(0^#(opp(x))) 738.64/297.04 , opp^#(#()) -> c_15() 738.64/297.04 , opp^#(1(x)) -> c_16(opp^#(x)) 738.64/297.04 , opp^#(j(x)) -> c_17(opp^#(x)) 738.64/297.04 , -^#(x, y) -> c_18(+^#(x, opp(y))) 738.64/297.04 , *^#(0(x), y) -> c_19(0^#(*(x, y))) 738.64/297.04 , *^#(#(), x) -> c_20() 738.64/297.04 , *^#(1(x), y) -> c_21(+^#(0(*(x, y)), y)) 738.64/297.04 , *^#(j(x), y) -> c_22(-^#(0(*(x, y)), y)) 738.64/297.04 , *^#(*(x, y), z) -> c_23(*^#(x, *(y, z))) } 738.64/297.04 738.64/297.04 and mark the set of starting terms. 738.64/297.04 738.64/297.04 We are left with following problem, upon which TcT provides the 738.64/297.04 certificate MAYBE. 738.64/297.04 738.64/297.04 Strict DPs: 738.64/297.04 { 0^#(#()) -> c_1() 738.64/297.04 , +^#(x, #()) -> c_2(x) 738.64/297.04 , +^#(0(x), 0(y)) -> c_3(0^#(+(x, y))) 738.64/297.04 , +^#(0(x), 1(y)) -> c_4(+^#(x, y)) 738.64/297.04 , +^#(0(x), j(y)) -> c_5(+^#(x, y)) 738.64/297.04 , +^#(#(), x) -> c_6(x) 738.64/297.04 , +^#(+(x, y), z) -> c_7(+^#(x, +(y, z))) 738.64/297.04 , +^#(1(x), 0(y)) -> c_8(+^#(x, y)) 738.64/297.04 , +^#(1(x), 1(y)) -> c_9(+^#(+(x, y), 1(#()))) 738.64/297.04 , +^#(1(x), j(y)) -> c_10(0^#(+(x, y))) 738.64/297.04 , +^#(j(x), 0(y)) -> c_11(+^#(x, y)) 738.64/297.04 , +^#(j(x), 1(y)) -> c_12(0^#(+(x, y))) 738.64/297.04 , +^#(j(x), j(y)) -> c_13(+^#(+(x, y), j(#()))) 738.64/297.04 , opp^#(0(x)) -> c_14(0^#(opp(x))) 738.64/297.04 , opp^#(#()) -> c_15() 738.64/297.04 , opp^#(1(x)) -> c_16(opp^#(x)) 738.64/297.04 , opp^#(j(x)) -> c_17(opp^#(x)) 738.64/297.04 , -^#(x, y) -> c_18(+^#(x, opp(y))) 738.64/297.04 , *^#(0(x), y) -> c_19(0^#(*(x, y))) 738.64/297.04 , *^#(#(), x) -> c_20() 738.64/297.04 , *^#(1(x), y) -> c_21(+^#(0(*(x, y)), y)) 738.64/297.04 , *^#(j(x), y) -> c_22(-^#(0(*(x, y)), y)) 738.64/297.04 , *^#(*(x, y), z) -> c_23(*^#(x, *(y, z))) } 738.64/297.04 Strict Trs: 738.64/297.04 { 0(#()) -> #() 738.64/297.04 , +(x, #()) -> x 738.64/297.04 , +(0(x), 0(y)) -> 0(+(x, y)) 738.64/297.04 , +(0(x), 1(y)) -> 1(+(x, y)) 738.64/297.04 , +(0(x), j(y)) -> j(+(x, y)) 738.64/297.04 , +(#(), x) -> x 738.64/297.04 , +(+(x, y), z) -> +(x, +(y, z)) 738.64/297.04 , +(1(x), 0(y)) -> 1(+(x, y)) 738.64/297.04 , +(1(x), 1(y)) -> j(+(+(x, y), 1(#()))) 738.64/297.04 , +(1(x), j(y)) -> 0(+(x, y)) 738.64/297.04 , +(j(x), 0(y)) -> j(+(x, y)) 738.64/297.04 , +(j(x), 1(y)) -> 0(+(x, y)) 738.64/297.04 , +(j(x), j(y)) -> 1(+(+(x, y), j(#()))) 738.64/297.04 , opp(0(x)) -> 0(opp(x)) 738.64/297.04 , opp(#()) -> #() 738.64/297.04 , opp(1(x)) -> j(opp(x)) 738.64/297.04 , opp(j(x)) -> 1(opp(x)) 738.64/297.04 , -(x, y) -> +(x, opp(y)) 738.64/297.04 , *(0(x), y) -> 0(*(x, y)) 738.64/297.04 , *(#(), x) -> #() 738.64/297.04 , *(1(x), y) -> +(0(*(x, y)), y) 738.64/297.04 , *(j(x), y) -> -(0(*(x, y)), y) 738.64/297.04 , *(*(x, y), z) -> *(x, *(y, z)) } 738.64/297.04 Obligation: 738.64/297.04 runtime complexity 738.64/297.04 Answer: 738.64/297.04 MAYBE 738.64/297.04 738.64/297.04 We estimate the number of application of {1,15,20} by applications 738.64/297.04 of Pre({1,15,20}) = {2,3,6,10,12,14,16,17,19,23}. Here rules are 738.64/297.04 labeled as follows: 738.64/297.04 738.64/297.04 DPs: 738.64/297.04 { 1: 0^#(#()) -> c_1() 738.64/297.04 , 2: +^#(x, #()) -> c_2(x) 738.64/297.04 , 3: +^#(0(x), 0(y)) -> c_3(0^#(+(x, y))) 738.64/297.04 , 4: +^#(0(x), 1(y)) -> c_4(+^#(x, y)) 738.64/297.04 , 5: +^#(0(x), j(y)) -> c_5(+^#(x, y)) 738.64/297.04 , 6: +^#(#(), x) -> c_6(x) 738.64/297.04 , 7: +^#(+(x, y), z) -> c_7(+^#(x, +(y, z))) 738.64/297.04 , 8: +^#(1(x), 0(y)) -> c_8(+^#(x, y)) 738.64/297.04 , 9: +^#(1(x), 1(y)) -> c_9(+^#(+(x, y), 1(#()))) 738.64/297.04 , 10: +^#(1(x), j(y)) -> c_10(0^#(+(x, y))) 738.64/297.04 , 11: +^#(j(x), 0(y)) -> c_11(+^#(x, y)) 738.64/297.04 , 12: +^#(j(x), 1(y)) -> c_12(0^#(+(x, y))) 738.64/297.04 , 13: +^#(j(x), j(y)) -> c_13(+^#(+(x, y), j(#()))) 738.64/297.04 , 14: opp^#(0(x)) -> c_14(0^#(opp(x))) 738.64/297.04 , 15: opp^#(#()) -> c_15() 738.64/297.04 , 16: opp^#(1(x)) -> c_16(opp^#(x)) 738.64/297.04 , 17: opp^#(j(x)) -> c_17(opp^#(x)) 738.64/297.04 , 18: -^#(x, y) -> c_18(+^#(x, opp(y))) 738.64/297.04 , 19: *^#(0(x), y) -> c_19(0^#(*(x, y))) 738.64/297.04 , 20: *^#(#(), x) -> c_20() 738.64/297.04 , 21: *^#(1(x), y) -> c_21(+^#(0(*(x, y)), y)) 738.64/297.04 , 22: *^#(j(x), y) -> c_22(-^#(0(*(x, y)), y)) 738.64/297.04 , 23: *^#(*(x, y), z) -> c_23(*^#(x, *(y, z))) } 738.64/297.04 738.64/297.04 We are left with following problem, upon which TcT provides the 738.64/297.04 certificate MAYBE. 738.64/297.04 738.64/297.04 Strict DPs: 738.64/297.04 { +^#(x, #()) -> c_2(x) 738.64/297.04 , +^#(0(x), 0(y)) -> c_3(0^#(+(x, y))) 738.64/297.04 , +^#(0(x), 1(y)) -> c_4(+^#(x, y)) 738.64/297.04 , +^#(0(x), j(y)) -> c_5(+^#(x, y)) 738.64/297.04 , +^#(#(), x) -> c_6(x) 738.64/297.04 , +^#(+(x, y), z) -> c_7(+^#(x, +(y, z))) 738.64/297.04 , +^#(1(x), 0(y)) -> c_8(+^#(x, y)) 738.64/297.04 , +^#(1(x), 1(y)) -> c_9(+^#(+(x, y), 1(#()))) 738.64/297.04 , +^#(1(x), j(y)) -> c_10(0^#(+(x, y))) 738.64/297.04 , +^#(j(x), 0(y)) -> c_11(+^#(x, y)) 738.64/297.04 , +^#(j(x), 1(y)) -> c_12(0^#(+(x, y))) 738.64/297.04 , +^#(j(x), j(y)) -> c_13(+^#(+(x, y), j(#()))) 738.64/297.04 , opp^#(0(x)) -> c_14(0^#(opp(x))) 738.64/297.04 , opp^#(1(x)) -> c_16(opp^#(x)) 738.64/297.04 , opp^#(j(x)) -> c_17(opp^#(x)) 738.64/297.04 , -^#(x, y) -> c_18(+^#(x, opp(y))) 738.64/297.04 , *^#(0(x), y) -> c_19(0^#(*(x, y))) 738.64/297.04 , *^#(1(x), y) -> c_21(+^#(0(*(x, y)), y)) 738.64/297.04 , *^#(j(x), y) -> c_22(-^#(0(*(x, y)), y)) 738.64/297.04 , *^#(*(x, y), z) -> c_23(*^#(x, *(y, z))) } 738.64/297.04 Strict Trs: 738.64/297.04 { 0(#()) -> #() 738.64/297.04 , +(x, #()) -> x 738.64/297.04 , +(0(x), 0(y)) -> 0(+(x, y)) 738.64/297.04 , +(0(x), 1(y)) -> 1(+(x, y)) 738.64/297.04 , +(0(x), j(y)) -> j(+(x, y)) 738.64/297.04 , +(#(), x) -> x 738.64/297.04 , +(+(x, y), z) -> +(x, +(y, z)) 738.64/297.04 , +(1(x), 0(y)) -> 1(+(x, y)) 738.64/297.04 , +(1(x), 1(y)) -> j(+(+(x, y), 1(#()))) 738.64/297.04 , +(1(x), j(y)) -> 0(+(x, y)) 738.64/297.04 , +(j(x), 0(y)) -> j(+(x, y)) 738.64/297.04 , +(j(x), 1(y)) -> 0(+(x, y)) 738.64/297.04 , +(j(x), j(y)) -> 1(+(+(x, y), j(#()))) 738.64/297.04 , opp(0(x)) -> 0(opp(x)) 738.64/297.04 , opp(#()) -> #() 738.64/297.04 , opp(1(x)) -> j(opp(x)) 738.64/297.04 , opp(j(x)) -> 1(opp(x)) 738.64/297.04 , -(x, y) -> +(x, opp(y)) 738.64/297.04 , *(0(x), y) -> 0(*(x, y)) 738.64/297.04 , *(#(), x) -> #() 738.64/297.04 , *(1(x), y) -> +(0(*(x, y)), y) 738.64/297.04 , *(j(x), y) -> -(0(*(x, y)), y) 738.64/297.04 , *(*(x, y), z) -> *(x, *(y, z)) } 738.64/297.04 Weak DPs: 738.64/297.04 { 0^#(#()) -> c_1() 738.64/297.04 , opp^#(#()) -> c_15() 738.64/297.04 , *^#(#(), x) -> c_20() } 738.64/297.04 Obligation: 738.64/297.04 runtime complexity 738.64/297.04 Answer: 738.64/297.04 MAYBE 738.64/297.04 738.64/297.04 We estimate the number of application of {2,9,11,13,17} by 738.64/297.04 applications of Pre({2,9,11,13,17}) = 738.64/297.04 {1,3,4,5,6,7,8,10,12,14,15,16,18,20}. Here rules are labeled as 738.64/297.04 follows: 738.64/297.04 738.64/297.04 DPs: 738.64/297.04 { 1: +^#(x, #()) -> c_2(x) 738.64/297.04 , 2: +^#(0(x), 0(y)) -> c_3(0^#(+(x, y))) 738.64/297.04 , 3: +^#(0(x), 1(y)) -> c_4(+^#(x, y)) 738.64/297.04 , 4: +^#(0(x), j(y)) -> c_5(+^#(x, y)) 738.64/297.04 , 5: +^#(#(), x) -> c_6(x) 738.64/297.04 , 6: +^#(+(x, y), z) -> c_7(+^#(x, +(y, z))) 738.64/297.04 , 7: +^#(1(x), 0(y)) -> c_8(+^#(x, y)) 738.64/297.04 , 8: +^#(1(x), 1(y)) -> c_9(+^#(+(x, y), 1(#()))) 738.64/297.04 , 9: +^#(1(x), j(y)) -> c_10(0^#(+(x, y))) 738.64/297.04 , 10: +^#(j(x), 0(y)) -> c_11(+^#(x, y)) 738.64/297.04 , 11: +^#(j(x), 1(y)) -> c_12(0^#(+(x, y))) 738.64/297.04 , 12: +^#(j(x), j(y)) -> c_13(+^#(+(x, y), j(#()))) 738.64/297.04 , 13: opp^#(0(x)) -> c_14(0^#(opp(x))) 738.64/297.04 , 14: opp^#(1(x)) -> c_16(opp^#(x)) 738.64/297.04 , 15: opp^#(j(x)) -> c_17(opp^#(x)) 738.64/297.04 , 16: -^#(x, y) -> c_18(+^#(x, opp(y))) 738.64/297.04 , 17: *^#(0(x), y) -> c_19(0^#(*(x, y))) 738.64/297.04 , 18: *^#(1(x), y) -> c_21(+^#(0(*(x, y)), y)) 738.64/297.04 , 19: *^#(j(x), y) -> c_22(-^#(0(*(x, y)), y)) 738.64/297.04 , 20: *^#(*(x, y), z) -> c_23(*^#(x, *(y, z))) 738.64/297.04 , 21: 0^#(#()) -> c_1() 738.64/297.04 , 22: opp^#(#()) -> c_15() 738.64/297.04 , 23: *^#(#(), x) -> c_20() } 738.64/297.04 738.64/297.04 We are left with following problem, upon which TcT provides the 738.64/297.04 certificate MAYBE. 738.64/297.04 738.64/297.04 Strict DPs: 738.64/297.04 { +^#(x, #()) -> c_2(x) 738.64/297.04 , +^#(0(x), 1(y)) -> c_4(+^#(x, y)) 738.64/297.04 , +^#(0(x), j(y)) -> c_5(+^#(x, y)) 738.64/297.04 , +^#(#(), x) -> c_6(x) 738.64/297.04 , +^#(+(x, y), z) -> c_7(+^#(x, +(y, z))) 738.64/297.04 , +^#(1(x), 0(y)) -> c_8(+^#(x, y)) 738.64/297.04 , +^#(1(x), 1(y)) -> c_9(+^#(+(x, y), 1(#()))) 738.64/297.04 , +^#(j(x), 0(y)) -> c_11(+^#(x, y)) 738.64/297.04 , +^#(j(x), j(y)) -> c_13(+^#(+(x, y), j(#()))) 738.64/297.04 , opp^#(1(x)) -> c_16(opp^#(x)) 738.64/297.04 , opp^#(j(x)) -> c_17(opp^#(x)) 738.64/297.04 , -^#(x, y) -> c_18(+^#(x, opp(y))) 738.64/297.04 , *^#(1(x), y) -> c_21(+^#(0(*(x, y)), y)) 738.64/297.04 , *^#(j(x), y) -> c_22(-^#(0(*(x, y)), y)) 738.64/297.04 , *^#(*(x, y), z) -> c_23(*^#(x, *(y, z))) } 738.64/297.04 Strict Trs: 738.64/297.04 { 0(#()) -> #() 738.64/297.04 , +(x, #()) -> x 738.64/297.04 , +(0(x), 0(y)) -> 0(+(x, y)) 738.64/297.04 , +(0(x), 1(y)) -> 1(+(x, y)) 738.64/297.04 , +(0(x), j(y)) -> j(+(x, y)) 738.64/297.04 , +(#(), x) -> x 738.64/297.04 , +(+(x, y), z) -> +(x, +(y, z)) 738.64/297.04 , +(1(x), 0(y)) -> 1(+(x, y)) 738.64/297.04 , +(1(x), 1(y)) -> j(+(+(x, y), 1(#()))) 738.64/297.04 , +(1(x), j(y)) -> 0(+(x, y)) 738.64/297.04 , +(j(x), 0(y)) -> j(+(x, y)) 738.64/297.04 , +(j(x), 1(y)) -> 0(+(x, y)) 738.64/297.04 , +(j(x), j(y)) -> 1(+(+(x, y), j(#()))) 738.64/297.04 , opp(0(x)) -> 0(opp(x)) 738.64/297.04 , opp(#()) -> #() 738.64/297.04 , opp(1(x)) -> j(opp(x)) 738.64/297.04 , opp(j(x)) -> 1(opp(x)) 738.64/297.04 , -(x, y) -> +(x, opp(y)) 738.64/297.04 , *(0(x), y) -> 0(*(x, y)) 738.64/297.04 , *(#(), x) -> #() 738.64/297.04 , *(1(x), y) -> +(0(*(x, y)), y) 738.64/297.04 , *(j(x), y) -> -(0(*(x, y)), y) 738.64/297.04 , *(*(x, y), z) -> *(x, *(y, z)) } 738.64/297.04 Weak DPs: 738.64/297.04 { 0^#(#()) -> c_1() 738.64/297.04 , +^#(0(x), 0(y)) -> c_3(0^#(+(x, y))) 738.64/297.04 , +^#(1(x), j(y)) -> c_10(0^#(+(x, y))) 738.64/297.04 , +^#(j(x), 1(y)) -> c_12(0^#(+(x, y))) 738.64/297.04 , opp^#(0(x)) -> c_14(0^#(opp(x))) 738.64/297.04 , opp^#(#()) -> c_15() 738.64/297.04 , *^#(0(x), y) -> c_19(0^#(*(x, y))) 738.64/297.04 , *^#(#(), x) -> c_20() } 738.64/297.04 Obligation: 738.64/297.04 runtime complexity 738.64/297.04 Answer: 738.64/297.04 MAYBE 738.64/297.04 738.64/297.04 Empty strict component of the problem is NOT empty. 738.64/297.04 738.64/297.04 738.64/297.04 Arrrr.. 738.86/297.21 EOF