Input TRS: 1: 0(\#()) -> \#() 2: +(\#(),x) -> x 3: +(x,\#()) -> x 4: +(0(x),0(y)) -> 0(+(x,y)) 5: +(0(x),1(y)) -> 1(+(x,y)) 6: +(1(x),0(y)) -> 1(+(x,y)) 7: +(1(x),1(y)) -> 0(+(+(x,y),1(\#()))) 8: +(+(x,y),z) -> +(x,+(y,z)) 9: -(\#(),x) -> \#() 10: -(x,\#()) -> x 11: -(0(x),0(y)) -> 0(-(x,y)) 12: -(0(x),1(y)) -> 1(-(-(x,y),1(\#()))) 13: -(1(x),0(y)) -> 1(-(x,y)) 14: -(1(x),1(y)) -> 0(-(x,y)) 15: not(true()) -> false() 16: not(false()) -> true() 17: if(true(),x,y) -> x 18: if(false(),x,y) -> y 19: ge(0(x),0(y)) -> ge(x,y) 20: ge(0(x),1(y)) -> not(ge(y,x)) 21: ge(1(x),0(y)) -> ge(x,y) 22: ge(1(x),1(y)) -> ge(x,y) 23: ge(x,\#()) -> true() 24: ge(\#(),0(x)) -> ge(\#(),x) 25: ge(\#(),1(x)) -> false() 26: log(x) -> -(log'(x),1(\#())) 27: log'(\#()) -> \#() 28: log'(1(x)) -> +(log'(x),1(\#())) 29: log'(0(x)) -> if(ge(x,1(\#())),+(log'(x),1(\#())),\#()) Number of strict rules: 29 Direct Order(PosReal,>,Poly) ... removes: 26 27 1(x1) weight: 2 * x1 false() weight: 0 \#() weight: 0 true() weight: 0 log(x1) weight: (/ 1 4) + x1 0(x1) weight: 2 * x1 if(x1,x2,x3) weight: x1 + x2 + x3 ge(x1,x2) weight: x1 + x2 -(x1,x2) weight: x1 + x2 +(x1,x2) weight: x1 + x2 log'(x1) weight: (/ 1 8) + x1 not(x1) weight: x1 Number of strict rules: 27 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #log'(0(x)) -> #if(ge(x,1(\#())),+(log'(x),1(\#())),\#()) #2: #log'(0(x)) -> #ge(x,1(\#())) #3: #log'(0(x)) -> #+(log'(x),1(\#())) #4: #log'(0(x)) -> #log'(x) #5: #+(1(x),0(y)) -> #+(x,y) #6: #-(1(x),0(y)) -> #-(x,y) #7: #-(0(x),0(y)) -> #0(-(x,y)) #8: #-(0(x),0(y)) -> #-(x,y) #9: #ge(\#(),0(x)) -> #ge(\#(),x) #10: #-(0(x),1(y)) -> #-(-(x,y),1(\#())) #11: #-(0(x),1(y)) -> #-(x,y) #12: #-(1(x),1(y)) -> #0(-(x,y)) #13: #-(1(x),1(y)) -> #-(x,y) #14: #ge(0(x),1(y)) -> #not(ge(y,x)) #15: #ge(0(x),1(y)) -> #ge(y,x) #16: #+(1(x),1(y)) -> #0(+(+(x,y),1(\#()))) #17: #+(1(x),1(y)) -> #+(+(x,y),1(\#())) #18: #+(1(x),1(y)) -> #+(x,y) #19: #+(0(x),1(y)) -> #+(x,y) #20: #log'(1(x)) -> #+(log'(x),1(\#())) #21: #log'(1(x)) -> #log'(x) #22: #ge(1(x),1(y)) -> #ge(x,y) #23: #ge(0(x),0(y)) -> #ge(x,y) #24: #ge(1(x),0(y)) -> #ge(x,y) #25: #+(+(x,y),z) -> #+(x,+(y,z)) #26: #+(+(x,y),z) -> #+(y,z) #27: #+(0(x),0(y)) -> #0(+(x,y)) #28: #+(0(x),0(y)) -> #+(x,y) Number of SCCs: 5, DPs: 19, edges: 91 SCC { #9 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #0(x1) weight: 0 1(x1) weight: 0 false() weight: 0 #ge(x1,x2) weight: x2 \#() weight: 0 true() weight: 0 #not(x1) weight: 0 log(x1) weight: 0 0(x1) weight: (/ 1 2) + x1 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 #log'(x1) weight: 0 -(x1,x2) weight: 0 #-(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 +(x1,x2) weight: 0 log'(x1) weight: 0 #+(x1,x2) weight: 0 not(x1) weight: 0 Usable rules: { } Removed DPs: #9 Number of SCCs: 4, DPs: 18, edges: 90 SCC { #4 #21 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #0(x1) weight: 0 1(x1) weight: (/ 1 2) + x1 false() weight: 0 #ge(x1,x2) weight: 0 \#() weight: 0 true() weight: 0 #not(x1) weight: 0 log(x1) weight: 0 0(x1) weight: (/ 1 2) + x1 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 #log'(x1) weight: x1 -(x1,x2) weight: 0 #-(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 +(x1,x2) weight: 0 log'(x1) weight: 0 #+(x1,x2) weight: 0 not(x1) weight: 0 Usable rules: { } Removed DPs: #4 #21 Number of SCCs: 3, DPs: 16, edges: 86 SCC { #15 #22..24 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #0(x1) weight: 0 1(x1) weight: (/ 1 4) + x1 false() weight: 0 #ge(x1,x2) weight: x1 + x2 \#() weight: 0 true() weight: 0 #not(x1) weight: 0 log(x1) weight: 0 0(x1) weight: (/ 1 4) + x1 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 #log'(x1) weight: 0 -(x1,x2) weight: 0 #-(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 +(x1,x2) weight: 0 log'(x1) weight: 0 #+(x1,x2) weight: 0 not(x1) weight: 0 Usable rules: { } Removed DPs: #15 #22..24 Number of SCCs: 2, DPs: 12, edges: 70 SCC { #6 #8 #10 #11 #13 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #0(x1) weight: 0 1(x1) weight: (/ 1 2) + x1 false() weight: 0 #ge(x1,x2) weight: 0 \#() weight: 0 true() weight: 0 #not(x1) weight: 0 log(x1) weight: 0 0(x1) weight: (/ 1 2) + x1 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 #log'(x1) weight: 0 -(x1,x2) weight: (/ 1 2) #-(x1,x2) weight: x2 #if(x1,x2,x3) weight: 0 +(x1,x2) weight: 0 log'(x1) weight: 0 #+(x1,x2) weight: 0 not(x1) weight: 0 Usable rules: { } Removed DPs: #6 #8 #11 #13 Number of SCCs: 2, DPs: 8, edges: 48 SCC { #10 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #0(x1) weight: 0 1(x1) weight: (/ 1 2) + x1 false() weight: 0 #ge(x1,x2) weight: 0 \#() weight: 0 true() weight: 0 #not(x1) weight: 0 log(x1) weight: 0 0(x1) weight: (/ 1 2) + x1 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 #log'(x1) weight: 0 -(x1,x2) weight: x1 #-(x1,x2) weight: x1 + x2 #if(x1,x2,x3) weight: 0 +(x1,x2) weight: 0 log'(x1) weight: 0 #+(x1,x2) weight: 0 not(x1) weight: 0 Usable rules: { 1 9..14 } Removed DPs: #10 Number of SCCs: 1, DPs: 7, edges: 47 SCC { #5 #17..19 #25 #26 #28 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #0(x1) weight: 0 1(x1) weight: (/ 1 4) + x1 false() weight: 0 #ge(x1,x2) weight: 0 \#() weight: 0 true() weight: 0 #not(x1) weight: 0 log(x1) weight: 0 0(x1) weight: (/ 1 8) + x1 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 #log'(x1) weight: 0 -(x1,x2) weight: (/ 1 8) #-(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 +(x1,x2) weight: (/ 1 8) + x1 + x2 log'(x1) weight: 0 #+(x1,x2) weight: x1 + x2 not(x1) weight: 0 Usable rules: { 1..8 } Removed DPs: #5 #17..19 #26 #28 Number of SCCs: 2, DPs: 1, edges: 1 SCC { #25 } Removing DPs: Order(PosReal,>,Sum)... succeeded. #0(x1) weight: 0 1(x1) weight: (/ 1 4) + x1 false() weight: 0 #ge(x1,x2) weight: 0 \#() weight: 0 true() weight: 0 #not(x1) weight: 0 log(x1) weight: 0 0(x1) weight: (/ 1 8) + x1 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 #log'(x1) weight: 0 -(x1,x2) weight: (/ 1 8) #-(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 +(x1,x2) weight: (/ 1 8) + x1 + x2 log'(x1) weight: 0 #+(x1,x2) weight: x1 not(x1) weight: 0 Usable rules: { 1..8 } Removed DPs: #25 Number of SCCs: 1, DPs: 0, edges: 0 YES