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
   |0|()	weight: 0
   Log(x1)	weight: (/ 81441 4) + 2 * x1
   and(x1,x2)	weight: (/ 127001 8) + x1 + x2
     r()	weight: 0
  Size(x1)	weight: (/ 215617 8) + 2 * x1
 false()	weight: 0
     l()	weight: 0
   Min(x1)	weight: (/ 1 8) + 2 * x1
     O(x1)	weight: 2 * x1
  true()	weight: 0
   Val(x1)	weight: x1
     I(x1)	weight: 2 * x1
    if(x1,x2,x3)	weight: 2 * x1 + x2 + 2 * x3
    ge(x1,x2)	weight: x1 + x2
    BS(x1)	weight: (/ 1 8) + x1
     -(x1,x2)	weight: x1 + x2
   |1|()	weight: 0
    WB(x1)	weight: (/ 1 8) + x1
     L(x1)	weight: (/ 1 8) + x1
     N(x1,x2,x3)	weight: (/ 1205087 4) + 2 * x1 + x2 + x3
     +(x1,x2)	weight: x1 + x2
|Log'|(x1)	weight: (/ 162881 8) + 2 * x1
   not(x1)	weight: x1
   Max(x1)	weight: (/ 1 8) + 2 * 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.
   |0|()	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
   Min(x1)	weight: 0
     O(x1)	weight: (/ 1 2) + x1
  true()	weight: 0
   Val(x1)	weight: 0
 #not(x1)	weight: 0
#|Log'|(x1)	weight: 0
     I(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
    BS(x1)	weight: 0
     -(x1,x2)	weight: 0
   |1|()	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
     +(x1,x2)	weight: 0
|Log'|(x1)	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.
   |0|()	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
   Min(x1)	weight: 0
     O(x1)	weight: (/ 1 2) + x1
  true()	weight: 0
   Val(x1)	weight: 0
 #not(x1)	weight: 0
#|Log'|(x1)	weight: x1
     I(x1)	weight: (/ 1 2) + x1
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
    BS(x1)	weight: 0
     -(x1,x2)	weight: 0
   |1|()	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
     +(x1,x2)	weight: 0
|Log'|(x1)	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.
   |0|()	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
   Min(x1)	weight: 0
     O(x1)	weight: (/ 1 4) + x1
  true()	weight: 0
   Val(x1)	weight: 0
 #not(x1)	weight: 0
#|Log'|(x1)	weight: 0
     I(x1)	weight: (/ 1 4) + x1
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
    BS(x1)	weight: 0
     -(x1,x2)	weight: 0
   |1|()	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
     +(x1,x2)	weight: 0
|Log'|(x1)	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.
   |0|()	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
   Min(x1)	weight: 0
     O(x1)	weight: (/ 1 2) + x1
  true()	weight: 0
   Val(x1)	weight: 0
 #not(x1)	weight: 0
#|Log'|(x1)	weight: 0
     I(x1)	weight: (/ 1 2) + x1
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
    BS(x1)	weight: 0
     -(x1,x2)	weight: (/ 1 2)
   |1|()	weight: 0
    WB(x1)	weight: 0
     L(x1)	weight: 0
     N(x1,x2,x3)	weight: 0
   #-(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
   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.
   |0|()	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
   Min(x1)	weight: 0
     O(x1)	weight: (/ 1 2) + x1
  true()	weight: 0
   Val(x1)	weight: 0
 #not(x1)	weight: 0
#|Log'|(x1)	weight: 0
     I(x1)	weight: (/ 1 2) + x1
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
    BS(x1)	weight: 0
     -(x1,x2)	weight: x1
   |1|()	weight: 0
    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
     +(x1,x2)	weight: 0
|Log'|(x1)	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.
   |0|()	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
   Min(x1)	weight: 0
     O(x1)	weight: (/ 1 2) + x1
  true()	weight: 0
   Val(x1)	weight: 0
 #not(x1)	weight: 0
#|Log'|(x1)	weight: 0
     I(x1)	weight: (/ 1 2) + x1
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
    BS(x1)	weight: 0
     -(x1,x2)	weight: x1
   |1|()	weight: 0
    WB(x1)	weight: 0
     L(x1)	weight: 0
     N(x1,x2,x3)	weight: 0
   #-(x1,x2)	weight: x1
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: (/ 1 2) + x1 + x2
|Log'|(x1)	weight: 0
   #+(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.
   |0|()	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
   Min(x1)	weight: 0
     O(x1)	weight: (/ 1 2) + x1
  true()	weight: 0
   Val(x1)	weight: 0
 #not(x1)	weight: 0
#|Log'|(x1)	weight: 0
     I(x1)	weight: (/ 1 2) + x1
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
    BS(x1)	weight: 0
     -(x1,x2)	weight: x1
   |1|()	weight: 0
    WB(x1)	weight: 0
     L(x1)	weight: 0
     N(x1,x2,x3)	weight: 0
   #-(x1,x2)	weight: x1
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: x1 + x2
|Log'|(x1)	weight: 0
   #+(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