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,|\#|()) -> x
    10: -(|\#|(),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(false()) -> true()
    16: not(true()) -> false()
    17: and(x,true()) -> x
    18: and(x,false()) -> false()
    19: if(true(),x,y) -> x
    20: if(false(),x,y) -> y
    21: ge(|0|(x),|0|(y)) -> ge(x,y)
    22: ge(|0|(x),|1|(y)) -> not(ge(y,x))
    23: ge(|1|(x),|0|(y)) -> ge(x,y)
    24: ge(|1|(x),|1|(y)) -> ge(x,y)
    25: ge(x,|\#|()) -> true()
    26: ge(|\#|(),|1|(x)) -> false()
    27: ge(|\#|(),|0|(x)) -> ge(|\#|(),x)
    28: val(l(x)) -> x
    29: val(n(x,y,z)) -> x
    30: min(l(x)) -> x
    31: min(n(x,y,z)) -> min(y)
    32: max(l(x)) -> x
    33: max(n(x,y,z)) -> max(z)
    34: bs(l(x)) -> true()
    35: bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
    36: size(l(x)) -> |1|(|\#|())
    37: size(n(x,y,z)) -> +(+(size(x),size(y)),|1|(|\#|()))
    38: wb(l(x)) -> true()
    39: wb(n(x,y,z)) -> and(if(ge(size(y),size(z)),ge(|1|(|\#|()),-(size(y),size(z))),ge(|1|(|\#|()),-(size(z),size(y)))),and(wb(y),wb(z)))
Number of strict rules: 39
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #bs(n(x,y,z)) -> #and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
   #2: #bs(n(x,y,z)) -> #and(ge(x,max(y)),ge(min(z),x))
   #3: #bs(n(x,y,z)) -> #ge(x,max(y))
   #4: #bs(n(x,y,z)) -> #max(y)
   #5: #bs(n(x,y,z)) -> #ge(min(z),x)
   #6: #bs(n(x,y,z)) -> #min(z)
   #7: #bs(n(x,y,z)) -> #and(bs(y),bs(z))
   #8: #bs(n(x,y,z)) -> #bs(y)
   #9: #bs(n(x,y,z)) -> #bs(z)
   #10: #size(n(x,y,z)) -> #+(+(size(x),size(y)),|1|(|\#|()))
   #11: #size(n(x,y,z)) -> #+(size(x),size(y))
   #12: #size(n(x,y,z)) -> #size(x)
   #13: #size(n(x,y,z)) -> #size(y)
   #14: #+(|1|(x),|0|(y)) -> #+(x,y)
   #15: #-(|1|(x),|0|(y)) -> #-(x,y)
   #16: #-(|0|(x),|0|(y)) -> #|0|(-(x,y))
   #17: #-(|0|(x),|0|(y)) -> #-(x,y)
   #18: #ge(|1|(x),|1|(y)) -> #ge(x,y)
   #19: #ge(|1|(x),|0|(y)) -> #ge(x,y)
   #20: #-(|0|(x),|1|(y)) -> #-(-(x,y),|1|(|\#|()))
   #21: #-(|0|(x),|1|(y)) -> #-(x,y)
   #22: #min(n(x,y,z)) -> #min(y)
   #23: #-(|1|(x),|1|(y)) -> #|0|(-(x,y))
   #24: #-(|1|(x),|1|(y)) -> #-(x,y)
   #25: #+(|1|(x),|1|(y)) -> #|0|(+(+(x,y),|1|(|\#|())))
   #26: #+(|1|(x),|1|(y)) -> #+(+(x,y),|1|(|\#|()))
   #27: #+(|1|(x),|1|(y)) -> #+(x,y)
   #28: #wb(n(x,y,z)) -> #and(if(ge(size(y),size(z)),ge(|1|(|\#|()),-(size(y),size(z))),ge(|1|(|\#|()),-(size(z),size(y)))),and(wb(y),wb(z)))
   #29: #wb(n(x,y,z)) -> #if(ge(size(y),size(z)),ge(|1|(|\#|()),-(size(y),size(z))),ge(|1|(|\#|()),-(size(z),size(y))))
   #30: #wb(n(x,y,z)) -> #ge(size(y),size(z))
   #31: #wb(n(x,y,z)) -> #size(y)
   #32: #wb(n(x,y,z)) -> #size(z)
   #33: #wb(n(x,y,z)) -> #ge(|1|(|\#|()),-(size(y),size(z)))
   #34: #wb(n(x,y,z)) -> #-(size(y),size(z))
   #35: #wb(n(x,y,z)) -> #size(y)
   #36: #wb(n(x,y,z)) -> #size(z)
   #37: #wb(n(x,y,z)) -> #ge(|1|(|\#|()),-(size(z),size(y)))
   #38: #wb(n(x,y,z)) -> #-(size(z),size(y))
   #39: #wb(n(x,y,z)) -> #size(z)
   #40: #wb(n(x,y,z)) -> #size(y)
   #41: #wb(n(x,y,z)) -> #and(wb(y),wb(z))
   #42: #wb(n(x,y,z)) -> #wb(y)
   #43: #wb(n(x,y,z)) -> #wb(z)
   #44: #max(n(x,y,z)) -> #max(z)
   #45: #+(|0|(x),|1|(y)) -> #+(x,y)
   #46: #ge(|0|(x),|1|(y)) -> #not(ge(y,x))
   #47: #ge(|0|(x),|1|(y)) -> #ge(y,x)
   #48: #ge(|\#|(),|0|(x)) -> #ge(|\#|(),x)
   #49: #ge(|0|(x),|0|(y)) -> #ge(x,y)
   #50: #+(x,+(y,z)) -> #+(+(x,y),z)
   #51: #+(x,+(y,z)) -> #+(x,y)
   #52: #+(|0|(x),|0|(y)) -> #|0|(+(x,y))
   #53: #+(|0|(x),|0|(y)) -> #+(x,y)
Number of SCCs: 9, DPs: 25, edges: 99
	SCC { #48 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 2) + x1
   val(x1)	weight: 0
 #|0|(x1)	weight: 0
     n(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: 0
     l(x1)	weight: 0
  #ge(x1,x2)	weight: x2
    wb(x1)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
#size(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
   max(x1)	weight: 0
 #max(x1)	weight: 0
     -(x1,x2)	weight: 0
   |1|(x1)	weight: 0
    bs(x1)	weight: 0
  #bs(x1)	weight: 0
   min(x1)	weight: 0
 #val(x1)	weight: 0
   #-(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: 0
  #wb(x1)	weight: 0
   #+(x1,x2)	weight: 0
 #and(x1,x2)	weight: 0
   not(x1)	weight: 0
  size(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { }
    Removed DPs: #48
Number of SCCs: 8, DPs: 24, edges: 98
	SCC { #44 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 2)
   val(x1)	weight: 0
 #|0|(x1)	weight: 0
     n(x1,x2,x3)	weight: (/ 1 2) + x3
   and(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: 0
     l(x1)	weight: 0
  #ge(x1,x2)	weight: 0
    wb(x1)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
#size(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
   max(x1)	weight: 0
 #max(x1)	weight: x1
     -(x1,x2)	weight: 0
   |1|(x1)	weight: 0
    bs(x1)	weight: 0
  #bs(x1)	weight: 0
   min(x1)	weight: 0
 #val(x1)	weight: 0
   #-(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: 0
  #wb(x1)	weight: 0
   #+(x1,x2)	weight: 0
 #and(x1,x2)	weight: 0
   not(x1)	weight: 0
  size(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { }
    Removed DPs: #44
Number of SCCs: 7, DPs: 23, edges: 97
	SCC { #22 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 2)
   val(x1)	weight: 0
 #|0|(x1)	weight: 0
     n(x1,x2,x3)	weight: (/ 1 2) + x2
   and(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: x1
     l(x1)	weight: 0
  #ge(x1,x2)	weight: 0
    wb(x1)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
#size(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
   max(x1)	weight: 0
 #max(x1)	weight: 0
     -(x1,x2)	weight: 0
   |1|(x1)	weight: 0
    bs(x1)	weight: 0
  #bs(x1)	weight: 0
   min(x1)	weight: 0
 #val(x1)	weight: 0
   #-(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: 0
  #wb(x1)	weight: 0
   #+(x1,x2)	weight: 0
 #and(x1,x2)	weight: 0
   not(x1)	weight: 0
  size(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { }
    Removed DPs: #22
Number of SCCs: 6, DPs: 22, edges: 96
	SCC { #12 #13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 2)
   val(x1)	weight: 0
 #|0|(x1)	weight: 0
     n(x1,x2,x3)	weight: (/ 1 2) + x1 + x2
   and(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: 0
     l(x1)	weight: 0
  #ge(x1,x2)	weight: 0
    wb(x1)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
#size(x1)	weight: x1
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
   max(x1)	weight: 0
 #max(x1)	weight: 0
     -(x1,x2)	weight: 0
   |1|(x1)	weight: 0
    bs(x1)	weight: 0
  #bs(x1)	weight: 0
   min(x1)	weight: 0
 #val(x1)	weight: 0
   #-(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: 0
  #wb(x1)	weight: 0
   #+(x1,x2)	weight: 0
 #and(x1,x2)	weight: 0
   not(x1)	weight: 0
  size(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { }
    Removed DPs: #12 #13
Number of SCCs: 5, DPs: 20, edges: 92
	SCC { #42 #43 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 2)
   val(x1)	weight: 0
 #|0|(x1)	weight: 0
     n(x1,x2,x3)	weight: (/ 1 2) + x2 + x3
   and(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: 0
     l(x1)	weight: 0
  #ge(x1,x2)	weight: 0
    wb(x1)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
#size(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
   max(x1)	weight: 0
 #max(x1)	weight: 0
     -(x1,x2)	weight: 0
   |1|(x1)	weight: 0
    bs(x1)	weight: 0
  #bs(x1)	weight: 0
   min(x1)	weight: 0
 #val(x1)	weight: 0
   #-(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: 0
  #wb(x1)	weight: x1
   #+(x1,x2)	weight: 0
 #and(x1,x2)	weight: 0
   not(x1)	weight: 0
  size(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { }
    Removed DPs: #42 #43
Number of SCCs: 4, DPs: 18, edges: 88
	SCC { #8 #9 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 2)
   val(x1)	weight: 0
 #|0|(x1)	weight: 0
     n(x1,x2,x3)	weight: (/ 1 2) + x2 + x3
   and(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: 0
     l(x1)	weight: 0
  #ge(x1,x2)	weight: 0
    wb(x1)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
#size(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
   max(x1)	weight: 0
 #max(x1)	weight: 0
     -(x1,x2)	weight: 0
   |1|(x1)	weight: 0
    bs(x1)	weight: 0
  #bs(x1)	weight: x1
   min(x1)	weight: 0
 #val(x1)	weight: 0
   #-(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: 0
  #wb(x1)	weight: 0
   #+(x1,x2)	weight: 0
 #and(x1,x2)	weight: 0
   not(x1)	weight: 0
  size(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { }
    Removed DPs: #8 #9
Number of SCCs: 3, DPs: 16, edges: 84
	SCC { #18 #19 #47 #49 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 4) + x1
   val(x1)	weight: 0
 #|0|(x1)	weight: 0
     n(x1,x2,x3)	weight: (/ 1 4)
   and(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: 0
     l(x1)	weight: 0
  #ge(x1,x2)	weight: x1 + x2
    wb(x1)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
#size(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
   max(x1)	weight: 0
 #max(x1)	weight: 0
     -(x1,x2)	weight: 0
   |1|(x1)	weight: (/ 1 4) + x1
    bs(x1)	weight: 0
  #bs(x1)	weight: 0
   min(x1)	weight: 0
 #val(x1)	weight: 0
   #-(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: 0
  #wb(x1)	weight: 0
   #+(x1,x2)	weight: 0
 #and(x1,x2)	weight: 0
   not(x1)	weight: 0
  size(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { }
    Removed DPs: #18 #19 #47 #49
Number of SCCs: 2, DPs: 12, edges: 68
	SCC { #15 #17 #20 #21 #24 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 2) + x1
   val(x1)	weight: 0
 #|0|(x1)	weight: 0
     n(x1,x2,x3)	weight: (/ 1 2)
   and(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: 0
     l(x1)	weight: 0
  #ge(x1,x2)	weight: 0
    wb(x1)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
#size(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
   max(x1)	weight: 0
 #max(x1)	weight: 0
     -(x1,x2)	weight: (/ 1 2)
   |1|(x1)	weight: (/ 1 2) + x1
    bs(x1)	weight: 0
  #bs(x1)	weight: 0
   min(x1)	weight: 0
 #val(x1)	weight: 0
   #-(x1,x2)	weight: x2
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: 0
  #wb(x1)	weight: 0
   #+(x1,x2)	weight: 0
 #and(x1,x2)	weight: 0
   not(x1)	weight: 0
  size(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { }
    Removed DPs: #15 #17 #21 #24
Number of SCCs: 2, DPs: 8, edges: 46
	SCC { #20 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 2) + x1
   val(x1)	weight: 0
 #|0|(x1)	weight: 0
     n(x1,x2,x3)	weight: (/ 1 2)
   and(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: 0
     l(x1)	weight: 0
  #ge(x1,x2)	weight: 0
    wb(x1)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
#size(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
   max(x1)	weight: 0
 #max(x1)	weight: 0
     -(x1,x2)	weight: x1
   |1|(x1)	weight: (/ 1 2) + x1
    bs(x1)	weight: 0
  #bs(x1)	weight: 0
   min(x1)	weight: 0
 #val(x1)	weight: 0
   #-(x1,x2)	weight: x1 + x2
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: 0
  #wb(x1)	weight: 0
   #+(x1,x2)	weight: 0
 #and(x1,x2)	weight: 0
   not(x1)	weight: 0
  size(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { 1 9..14 }
    Removed DPs: #20
Number of SCCs: 1, DPs: 7, edges: 45
	SCC { #14 #26 #27 #45 #50 #51 #53 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 2) + x1
   val(x1)	weight: 0
 #|0|(x1)	weight: 0
     n(x1,x2,x3)	weight: (/ 1 2)
   and(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: 0
     l(x1)	weight: 0
  #ge(x1,x2)	weight: 0
    wb(x1)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
#size(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
   max(x1)	weight: 0
 #max(x1)	weight: 0
     -(x1,x2)	weight: x1
   |1|(x1)	weight: (/ 1 2) + x1
    bs(x1)	weight: 0
  #bs(x1)	weight: 0
   min(x1)	weight: 0
 #val(x1)	weight: 0
   #-(x1,x2)	weight: x1
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: (/ 1 2) + x1 + x2
  #wb(x1)	weight: 0
   #+(x1,x2)	weight: x2
 #and(x1,x2)	weight: 0
   not(x1)	weight: 0
  size(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { 1 }
    Removed DPs: #14 #27 #45 #50 #51 #53
Number of SCCs: 2, DPs: 1, edges: 1
	SCC { #26 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 2) + x1
   val(x1)	weight: 0
 #|0|(x1)	weight: 0
     n(x1,x2,x3)	weight: (/ 1 2)
   and(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: 0
     l(x1)	weight: 0
  #ge(x1,x2)	weight: 0
    wb(x1)	weight: 0
  true()	weight: 0
 #not(x1)	weight: 0
#size(x1)	weight: 0
    if(x1,x2,x3)	weight: 0
    ge(x1,x2)	weight: 0
   max(x1)	weight: 0
 #max(x1)	weight: 0
     -(x1,x2)	weight: x1
   |1|(x1)	weight: (/ 1 2) + x1
    bs(x1)	weight: 0
  #bs(x1)	weight: 0
   min(x1)	weight: 0
 #val(x1)	weight: 0
   #-(x1,x2)	weight: x1
  #if(x1,x2,x3)	weight: 0
     +(x1,x2)	weight: x1 + x2
  #wb(x1)	weight: 0
   #+(x1,x2)	weight: x1 + x2
 #and(x1,x2)	weight: 0
   not(x1)	weight: 0
  size(x1)	weight: 0
   |\#|()	weight: 0
    Usable rules: { 1..8 }
    Removed DPs: #26
Number of SCCs: 1, DPs: 0, edges: 0
YES