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