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: +(|0|(x),j(y)) -> j(+(x,y))
    8: +(j(x),|0|(y)) -> j(+(x,y))
    9: +(|1|(x),|1|(y)) -> j(+(+(x,y),|1|(|\#|())))
    10: +(j(x),j(y)) -> |1|(+(+(x,y),j(|\#|())))
    11: +(|1|(x),j(y)) -> |0|(+(x,y))
    12: +(j(x),|1|(y)) -> |0|(+(x,y))
    13: +(+(x,y),z) -> +(x,+(y,z))
    14: opp(|\#|()) -> |\#|()
    15: opp(|0|(x)) -> |0|(opp(x))
    16: opp(|1|(x)) -> j(opp(x))
    17: opp(j(x)) -> |1|(opp(x))
    18: -(x,y) -> +(x,opp(y))
    19: *(|\#|(),x) -> |\#|()
    20: *(|0|(x),y) -> |0|(*(x,y))
    21: *(|1|(x),y) -> +(|0|(*(x,y)),y)
    22: *(j(x),y) -> -(|0|(*(x,y)),y)
    23: *(*(x,y),z) -> *(x,*(y,z))
    24: *(+(x,y),z) -> +(*(x,z),*(y,z))
    25: *(x,+(y,z)) -> +(*(x,y),*(x,z))
Number of strict rules: 25
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #+(|1|(x),|0|(y)) -> #+(x,y)
   #2: #+(+(x,y),z) -> #+(x,+(y,z))
   #3: #+(+(x,y),z) -> #+(y,z)
   #4: #+(|1|(x),|1|(y)) -> #+(+(x,y),|1|(|\#|()))
   #5: #+(|1|(x),|1|(y)) -> #+(x,y)
   #6: #+(|1|(x),j(y)) -> #|0|(+(x,y))
   #7: #+(|1|(x),j(y)) -> #+(x,y)
   #8: #*(+(x,y),z) -> #+(*(x,z),*(y,z))
   #9: #*(+(x,y),z) -> #*(x,z)
   #10: #*(+(x,y),z) -> #*(y,z)
   #11: #*(*(x,y),z) -> #*(x,*(y,z))
   #12: #*(*(x,y),z) -> #*(y,z)
   #13: #+(j(x),|1|(y)) -> #|0|(+(x,y))
   #14: #+(j(x),|1|(y)) -> #+(x,y)
   #15: #*(x,+(y,z)) -> #+(*(x,y),*(x,z))
   #16: #*(x,+(y,z)) -> #*(x,y)
   #17: #*(x,+(y,z)) -> #*(x,z)
   #18: #*(|0|(x),y) -> #|0|(*(x,y))
   #19: #*(|0|(x),y) -> #*(x,y)
   #20: #+(|0|(x),j(y)) -> #+(x,y)
   #21: #+(j(x),j(y)) -> #+(+(x,y),j(|\#|()))
   #22: #+(j(x),j(y)) -> #+(x,y)
   #23: #+(|0|(x),|1|(y)) -> #+(x,y)
   #24: #*(j(x),y) -> #-(|0|(*(x,y)),y)
   #25: #*(j(x),y) -> #|0|(*(x,y))
   #26: #*(j(x),y) -> #*(x,y)
   #27: #opp(j(x)) -> #opp(x)
   #28: #*(|1|(x),y) -> #+(|0|(*(x,y)),y)
   #29: #*(|1|(x),y) -> #|0|(*(x,y))
   #30: #*(|1|(x),y) -> #*(x,y)
   #31: #opp(|1|(x)) -> #opp(x)
   #32: #+(j(x),|0|(y)) -> #+(x,y)
   #33: #opp(|0|(x)) -> #|0|(opp(x))
   #34: #opp(|0|(x)) -> #opp(x)
   #35: #+(|0|(x),|0|(y)) -> #|0|(+(x,y))
   #36: #+(|0|(x),|0|(y)) -> #+(x,y)
   #37: #-(x,y) -> #+(x,opp(y))
   #38: #-(x,y) -> #opp(y)
Number of SCCs: 3, DPs: 25, edges: 245
	SCC { #27 #31 #34 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 2) + x1
 #|0|(x1)	weight: 0
   #*(x1,x2)	weight: 0
 #opp(x1)	weight: x1
     -(x1,x2)	weight: 0
   |1|(x1)	weight: (/ 1 2) + x1
     j(x1)	weight: (/ 1 2) + x1
   opp(x1)	weight: 0
   #-(x1,x2)	weight: 0
     +(x1,x2)	weight: 0
   #+(x1,x2)	weight: 0
     *(x1,x2)	weight: 0
   |\#|()	weight: 0
    Usable rules: { }
    Removed DPs: #27 #31 #34
Number of SCCs: 2, DPs: 22, edges: 236
	SCC { #9..12 #16 #17 #19 #26 #30 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 3 8) + x1
 #|0|(x1)	weight: 0
   #*(x1,x2)	weight: x1
 #opp(x1)	weight: 0
     -(x1,x2)	weight: x1
   |1|(x1)	weight: (/ 1 8) + x1
     j(x1)	weight: (/ 1 8) + x1
   opp(x1)	weight: (/ 1 8)
   #-(x1,x2)	weight: 0
     +(x1,x2)	weight: (/ 1 8) + x1 + x2
   #+(x1,x2)	weight: 0
     *(x1,x2)	weight: (/ 1 8) + x1 + x2
   |\#|()	weight: 0
    Usable rules: { }
    Removed DPs: #9..12 #19 #26 #30
Number of SCCs: 2, DPs: 15, edges: 159
	SCC { #16 #17 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|(x1)	weight: 0
 #|0|(x1)	weight: 0
   #*(x1,x2)	weight: max{0, (/ 1 4) + x2}
 #opp(x1)	weight: 0
     -(x1,x2)	weight: 0
   |1|(x1)	weight: 0
     j(x1)	weight: 0
   opp(x1)	weight: 0
   #-(x1,x2)	weight: 0
     +(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 4) + x1}
   #+(x1,x2)	weight: 0
     *(x1,x2)	weight: 0
   |\#|()	weight: 0
    Usable rules: { }
    Removed DPs: #16 #17
Number of SCCs: 1, DPs: 13, edges: 155
	SCC { #1..5 #7 #14 #20..23 #32 #36 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 4) + x1
 #|0|(x1)	weight: 0
   #*(x1,x2)	weight: 0
 #opp(x1)	weight: 0
     -(x1,x2)	weight: (/ 1 4)
   |1|(x1)	weight: (/ 1 4) + x1
     j(x1)	weight: (/ 1 4) + x1
   opp(x1)	weight: (/ 1 2)
   #-(x1,x2)	weight: 0
     +(x1,x2)	weight: x1 + x2
   #+(x1,x2)	weight: x1 + x2
     *(x1,x2)	weight: x2
   |\#|()	weight: 0
    Usable rules: { 1..13 }
    Removed DPs: #1 #4 #5 #7 #14 #20..23 #32 #36
Number of SCCs: 2, DPs: 2, edges: 4
	SCC { #2 #3 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|(x1)	weight: (/ 1 4)
 #|0|(x1)	weight: 0
   #*(x1,x2)	weight: 0
 #opp(x1)	weight: 0
     -(x1,x2)	weight: (/ 1 4)
   |1|(x1)	weight: (/ 1 4)
     j(x1)	weight: (/ 1 4)
   opp(x1)	weight: 0
   #-(x1,x2)	weight: 0
     +(x1,x2)	weight: (/ 1 2) + x1 + x2
   #+(x1,x2)	weight: x1
     *(x1,x2)	weight: x2
   |\#|()	weight: 0
    Usable rules: { 1..13 }
    Removed DPs: #2 #3
Number of SCCs: 1, DPs: 0, edges: 0
YES