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
   |0|(x1)	weight: 2 * x1
 false()	weight: 0
  true()	weight: 0
   log(x1)	weight: 23505 + 2 * x1
    if(x1,x2,x3)	weight: x1 + x2 + x3
    ge(x1,x2)	weight: x1 + x2
     -(x1,x2)	weight: x1 + x2
   |1|(x1)	weight: 2 * x1
     +(x1,x2)	weight: x1 + x2
|log'|(x1)	weight: (/ 47009 2) + x1
   not(x1)	weight: x1
   |\#|()	weight: 0
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: (/ 1 2) + x1
 #|0|(x1)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: x2
  true()	weight: 0
 #not(x1)	weight: 0
   log(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
     -(x1,x2)	weight: 0
   |1|(x1)	weight: 0
   #-(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#|log'|(x1)	weight: 0
     +(x1,x2)	weight: 0
|log'|(x1)	weight: 0
   #+(x1,x2)	weight: 0
   not(x1)	weight: 0
   |\#|()	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: (/ 1 2) + x1
 #|0|(x1)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
   log(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
     -(x1,x2)	weight: 0
   |1|(x1)	weight: (/ 1 2) + x1
   #-(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#|log'|(x1)	weight: x1
     +(x1,x2)	weight: 0
|log'|(x1)	weight: 0
   #+(x1,x2)	weight: 0
   not(x1)	weight: 0
   |\#|()	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: (/ 1 4) + x1
 #|0|(x1)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: x1 + x2
  true()	weight: 0
 #not(x1)	weight: 0
   log(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
     -(x1,x2)	weight: 0
   |1|(x1)	weight: (/ 1 4) + x1
   #-(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#|log'|(x1)	weight: 0
     +(x1,x2)	weight: 0
|log'|(x1)	weight: 0
   #+(x1,x2)	weight: 0
   not(x1)	weight: 0
   |\#|()	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: (/ 1 2) + x1
 #|0|(x1)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
   log(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
     -(x1,x2)	weight: (/ 1 2)
   |1|(x1)	weight: (/ 1 2) + x1
   #-(x1,x2)	weight: x2
  #if(x1,x2,x3)	weight: 0
#|log'|(x1)	weight: 0
     +(x1,x2)	weight: 0
|log'|(x1)	weight: 0
   #+(x1,x2)	weight: 0
   not(x1)	weight: 0
   |\#|()	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: (/ 1 2) + x1
 #|0|(x1)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
   log(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
     -(x1,x2)	weight: x1
   |1|(x1)	weight: (/ 1 2) + x1
   #-(x1,x2)	weight: x1 + x2
  #if(x1,x2,x3)	weight: 0
#|log'|(x1)	weight: 0
     +(x1,x2)	weight: 0
|log'|(x1)	weight: 0
   #+(x1,x2)	weight: 0
   not(x1)	weight: 0
   |\#|()	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: (/ 1 4) + x1
 #|0|(x1)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
   log(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
     -(x1,x2)	weight: x1
   |1|(x1)	weight: (/ 1 4) + x1
   #-(x1,x2)	weight: x1
  #if(x1,x2,x3)	weight: 0
#|log'|(x1)	weight: 0
     +(x1,x2)	weight: x1 + x2
|log'|(x1)	weight: 0
   #+(x1,x2)	weight: x1 + x2
   not(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { 1..8 }
    Removed DPs: #5 #17..19 #28
Number of SCCs: 2, DPs: 2, edges: 4
	SCC { #25 #26 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 8) + x1
 #|0|(x1)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
   log(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
     -(x1,x2)	weight: x1
   |1|(x1)	weight: (/ 1 4) + x1
   #-(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#|log'|(x1)	weight: 0
     +(x1,x2)	weight: (/ 1 8) + x1 + x2
|log'|(x1)	weight: 0
   #+(x1,x2)	weight: x1
   not(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { 1..8 }
    Removed DPs: #25 #26
Number of SCCs: 1, DPs: 0, edges: 0
YES