Input TRS: 1: O(0()) -> 0() 2: +(0(),x) -> x 3: +(x,0()) -> x 4: +(O(x),O(y)) -> O(+(x,y)) 5: +(O(x),I(y)) -> I(+(x,y)) 6: +(I(x),O(y)) -> I(+(x,y)) 7: +(I(x),I(y)) -> O(+(+(x,y),I(0()))) 8: +(x,+(y,z)) -> +(+(x,y),z) 9: -(x,0()) -> x 10: -(0(),x) -> 0() 11: -(O(x),O(y)) -> O(-(x,y)) 12: -(O(x),I(y)) -> I(-(-(x,y),I(1()))) 13: -(I(x),O(y)) -> I(-(x,y)) 14: -(I(x),I(y)) -> O(-(x,y)) 15: not(true()) -> false() 16: not(false()) -> true() 17: and(x,true()) -> x 18: and(x,false()) -> false() 19: if(true(),x,y) -> x 20: if(false(),x,y) -> y 21: ge(O(x),O(y)) -> ge(x,y) 22: ge(O(x),I(y)) -> not(ge(y,x)) 23: ge(I(x),O(y)) -> ge(x,y) 24: ge(I(x),I(y)) -> ge(x,y) 25: ge(x,0()) -> true() 26: ge(0(),O(x)) -> ge(0(),x) 27: ge(0(),I(x)) -> false() 28: Log'(0()) -> 0() 29: Log'(I(x)) -> +(Log'(x),I(0())) 30: Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),0()) 31: Log(x) -> -(Log'(x),I(0())) 32: Val(L(x)) -> x 33: Val(N(x,l(),r())) -> x 34: Min(L(x)) -> x 35: Min(N(x,l(),r())) -> Min(l()) 36: Max(L(x)) -> x 37: Max(N(x,l(),r())) -> Max(r()) 38: BS(L(x)) -> true() 39: BS(N(x,l(),r())) -> and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r()))) 40: Size(L(x)) -> I(0()) 41: Size(N(x,l(),r())) -> +(+(Size(l()),Size(r())),I(1())) 42: WB(L(x)) -> true() 43: WB(N(x,l(),r())) -> and(if(ge(Size(l()),Size(r())),ge(I(0()),-(Size(l()),Size(r()))),ge(I(0()),-(Size(r()),Size(l())))),and(WB(l()),WB(r()))) Number of strict rules: 43 Direct Order(PosReal,>,Poly) ... removes: 18 36 32 17 34 28 33 39 31 40 38 37 41 42 35 43 1() weight: 0 Log(x1) weight: (/ 1 64) + x1 and(x1,x2) weight: (/ 1 128) + x1 + x2 r() weight: 0 Size(x1) weight: (/ 1 128) + 2 * x1 false() weight: 0 l() weight: 0 Min(x1) weight: (/ 1 128) + x1 O(x1) weight: 2 * x1 true() weight: 0 Val(x1) weight: 2 * x1 I(x1) weight: 2 * x1 0() weight: 0 if(x1,x2,x3) weight: x1 + x2 + x3 ge(x1,x2) weight: x1 + x2 BS(x1) weight: (/ 1 128) + 2 * x1 -(x1,x2) weight: x1 + 2 * x2 WB(x1) weight: (/ 1 128) + 2 * x1 L(x1) weight: (/ 1 128) + x1 N(x1,x2,x3) weight: (/ 3 64) + 2 * x1 + x2 + x3 Log'(x1) weight: (/ 1 128) + x1 +(x1,x2) weight: x1 + x2 not(x1) weight: x1 Max(x1) weight: (/ 1 128) + x1 Number of strict rules: 27 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #Log'(I(x)) -> #+(Log'(x),I(0())) #2: #Log'(I(x)) -> #Log'(x) #3: #+(I(x),O(y)) -> #+(x,y) #4: #-(I(x),O(y)) -> #-(x,y) #5: #-(O(x),O(y)) -> #O(-(x,y)) #6: #-(O(x),O(y)) -> #-(x,y) #7: #ge(I(x),I(y)) -> #ge(x,y) #8: #ge(I(x),O(y)) -> #ge(x,y) #9: #-(O(x),I(y)) -> #-(-(x,y),I(1())) #10: #-(O(x),I(y)) -> #-(x,y) #11: #-(I(x),I(y)) -> #O(-(x,y)) #12: #-(I(x),I(y)) -> #-(x,y) #13: #Log'(O(x)) -> #if(ge(x,I(0())),+(Log'(x),I(0())),0()) #14: #Log'(O(x)) -> #ge(x,I(0())) #15: #Log'(O(x)) -> #+(Log'(x),I(0())) #16: #Log'(O(x)) -> #Log'(x) #17: #+(I(x),I(y)) -> #O(+(+(x,y),I(0()))) #18: #+(I(x),I(y)) -> #+(+(x,y),I(0())) #19: #+(I(x),I(y)) -> #+(x,y) #20: #+(O(x),I(y)) -> #+(x,y) #21: #ge(O(x),I(y)) -> #not(ge(y,x)) #22: #ge(O(x),I(y)) -> #ge(y,x) #23: #ge(0(),O(x)) -> #ge(0(),x) #24: #ge(O(x),O(y)) -> #ge(x,y) #25: #+(x,+(y,z)) -> #+(+(x,y),z) #26: #+(x,+(y,z)) -> #+(x,y) #27: #+(O(x),O(y)) -> #O(+(x,y)) #28: #+(O(x),O(y)) -> #+(x,y) Number of SCCs: 5, DPs: 19, edges: 89 SCC { #23 } Removing DPs: Order(PosReal,>,Sum)... succeeded. 1() weight: 0 #O(x1) weight: 0 Log(x1) weight: 0 and(x1,x2) weight: 0 r() weight: 0 Size(x1) weight: 0 false() weight: 0 l() weight: 0 #ge(x1,x2) weight: x2 #Log'(x1) weight: 0 Min(x1) weight: 0 O(x1) weight: (/ 1 2) + x1 true() weight: 0 Val(x1) weight: 0 #not(x1) weight: 0 I(x1) weight: 0 0() weight: 0 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 BS(x1) weight: 0 -(x1,x2) weight: 0 WB(x1) weight: 0 L(x1) weight: 0 N(x1,x2,x3) weight: 0 #-(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 Log'(x1) weight: 0 +(x1,x2) weight: 0 #+(x1,x2) weight: 0 not(x1) weight: 0 Max(x1) weight: 0 Usable rules: { } Removed DPs: #23 Number of SCCs: 4, DPs: 18, edges: 88 SCC { #2 #16 } Removing DPs: Order(PosReal,>,Sum)... succeeded. 1() weight: 0 #O(x1) weight: 0 Log(x1) weight: 0 and(x1,x2) weight: 0 r() weight: 0 Size(x1) weight: 0 false() weight: 0 l() weight: 0 #ge(x1,x2) weight: 0 #Log'(x1) weight: x1 Min(x1) weight: 0 O(x1) weight: (/ 1 2) + x1 true() weight: 0 Val(x1) weight: 0 #not(x1) weight: 0 I(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 BS(x1) weight: 0 -(x1,x2) weight: 0 WB(x1) weight: 0 L(x1) weight: 0 N(x1,x2,x3) weight: 0 #-(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 Log'(x1) weight: 0 +(x1,x2) weight: 0 #+(x1,x2) weight: 0 not(x1) weight: 0 Max(x1) weight: 0 Usable rules: { } Removed DPs: #2 #16 Number of SCCs: 3, DPs: 16, edges: 84 SCC { #7 #8 #22 #24 } Removing DPs: Order(PosReal,>,Sum)... succeeded. 1() weight: 0 #O(x1) weight: 0 Log(x1) weight: 0 and(x1,x2) weight: 0 r() weight: 0 Size(x1) weight: 0 false() weight: 0 l() weight: 0 #ge(x1,x2) weight: x1 + x2 #Log'(x1) weight: 0 Min(x1) weight: 0 O(x1) weight: (/ 1 4) + x1 true() weight: 0 Val(x1) weight: 0 #not(x1) weight: 0 I(x1) weight: (/ 1 4) + x1 0() weight: 0 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 BS(x1) weight: 0 -(x1,x2) weight: 0 WB(x1) weight: 0 L(x1) weight: 0 N(x1,x2,x3) weight: 0 #-(x1,x2) weight: 0 #if(x1,x2,x3) weight: 0 Log'(x1) weight: 0 +(x1,x2) weight: 0 #+(x1,x2) weight: 0 not(x1) weight: 0 Max(x1) weight: 0 Usable rules: { } Removed DPs: #7 #8 #22 #24 Number of SCCs: 2, DPs: 12, edges: 68 SCC { #4 #6 #9 #10 #12 } Removing DPs: Order(PosReal,>,Sum)... succeeded. 1() weight: 0 #O(x1) weight: 0 Log(x1) weight: 0 and(x1,x2) weight: 0 r() weight: 0 Size(x1) weight: 0 false() weight: 0 l() weight: 0 #ge(x1,x2) weight: 0 #Log'(x1) weight: 0 Min(x1) weight: 0 O(x1) weight: (/ 1 2) + x1 true() weight: 0 Val(x1) weight: 0 #not(x1) weight: 0 I(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 BS(x1) weight: 0 -(x1,x2) weight: (/ 1 2) WB(x1) weight: 0 L(x1) weight: 0 N(x1,x2,x3) weight: 0 #-(x1,x2) weight: x2 #if(x1,x2,x3) weight: 0 Log'(x1) weight: 0 +(x1,x2) weight: 0 #+(x1,x2) weight: 0 not(x1) weight: 0 Max(x1) weight: 0 Usable rules: { } Removed DPs: #4 #6 #10 #12 Number of SCCs: 2, DPs: 8, edges: 46 SCC { #9 } Removing DPs: Order(PosReal,>,Sum)... succeeded. 1() weight: 0 #O(x1) weight: 0 Log(x1) weight: 0 and(x1,x2) weight: 0 r() weight: 0 Size(x1) weight: 0 false() weight: 0 l() weight: 0 #ge(x1,x2) weight: 0 #Log'(x1) weight: 0 Min(x1) weight: 0 O(x1) weight: (/ 1 2) + x1 true() weight: 0 Val(x1) weight: 0 #not(x1) weight: 0 I(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 BS(x1) weight: 0 -(x1,x2) weight: x1 WB(x1) weight: 0 L(x1) weight: 0 N(x1,x2,x3) weight: 0 #-(x1,x2) weight: x1 + x2 #if(x1,x2,x3) weight: 0 Log'(x1) weight: 0 +(x1,x2) weight: 0 #+(x1,x2) weight: 0 not(x1) weight: 0 Max(x1) weight: 0 Usable rules: { 1 9..14 } Removed DPs: #9 Number of SCCs: 1, DPs: 7, edges: 45 SCC { #3 #18..20 #25 #26 #28 } Removing DPs: Order(PosReal,>,Sum)... succeeded. 1() weight: 0 #O(x1) weight: 0 Log(x1) weight: 0 and(x1,x2) weight: 0 r() weight: 0 Size(x1) weight: 0 false() weight: 0 l() weight: 0 #ge(x1,x2) weight: 0 #Log'(x1) weight: 0 Min(x1) weight: 0 O(x1) weight: (/ 1 2) + x1 true() weight: 0 Val(x1) weight: 0 #not(x1) weight: 0 I(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 BS(x1) weight: 0 -(x1,x2) weight: x1 WB(x1) weight: 0 L(x1) weight: 0 N(x1,x2,x3) weight: 0 #-(x1,x2) weight: x1 #if(x1,x2,x3) weight: 0 Log'(x1) weight: 0 +(x1,x2) weight: (/ 1 2) + x1 + x2 #+(x1,x2) weight: x2 not(x1) weight: 0 Max(x1) weight: 0 Usable rules: { 1 } Removed DPs: #3 #19 #20 #25 #26 #28 Number of SCCs: 2, DPs: 1, edges: 1 SCC { #18 } Removing DPs: Order(PosReal,>,Sum)... succeeded. 1() weight: 0 #O(x1) weight: 0 Log(x1) weight: 0 and(x1,x2) weight: 0 r() weight: 0 Size(x1) weight: 0 false() weight: 0 l() weight: 0 #ge(x1,x2) weight: 0 #Log'(x1) weight: 0 Min(x1) weight: 0 O(x1) weight: (/ 1 2) + x1 true() weight: 0 Val(x1) weight: 0 #not(x1) weight: 0 I(x1) weight: (/ 1 2) + x1 0() weight: 0 if(x1,x2,x3) weight: 0 ge(x1,x2) weight: 0 BS(x1) weight: 0 -(x1,x2) weight: x1 WB(x1) weight: 0 L(x1) weight: 0 N(x1,x2,x3) weight: 0 #-(x1,x2) weight: x1 #if(x1,x2,x3) weight: 0 Log'(x1) weight: 0 +(x1,x2) weight: x1 + x2 #+(x1,x2) weight: x1 + x2 not(x1) weight: 0 Max(x1) weight: 0 Usable rules: { 1..8 } Removed DPs: #18 Number of SCCs: 1, DPs: 0, edges: 0 YES