Input TRS:
    1: +(|0|(),|0|()) -> |0|()
    2: +(|0|(),|1|()) -> |1|()
    3: +(|0|(),|2|()) -> |2|()
    4: +(|0|(),|3|()) -> |3|()
    5: +(|0|(),|4|()) -> |4|()
    6: +(|0|(),|5|()) -> |5|()
    7: +(|0|(),|6|()) -> |6|()
    8: +(|0|(),|7|()) -> |7|()
    9: +(|0|(),|8|()) -> |8|()
    10: +(|0|(),|9|()) -> |9|()
    11: +(|1|(),|0|()) -> |1|()
    12: +(|1|(),|1|()) -> |2|()
    13: +(|1|(),|2|()) -> |3|()
    14: +(|1|(),|3|()) -> |4|()
    15: +(|1|(),|4|()) -> |5|()
    16: +(|1|(),|5|()) -> |6|()
    17: +(|1|(),|6|()) -> |7|()
    18: +(|1|(),|7|()) -> |8|()
    19: +(|1|(),|8|()) -> |9|()
    20: +(|1|(),|9|()) -> c(|1|(),|0|())
    21: +(|2|(),|0|()) -> |2|()
    22: +(|2|(),|1|()) -> |3|()
    23: +(|2|(),|2|()) -> |4|()
    24: +(|2|(),|3|()) -> |5|()
    25: +(|2|(),|4|()) -> |6|()
    26: +(|2|(),|5|()) -> |7|()
    27: +(|2|(),|6|()) -> |8|()
    28: +(|2|(),|7|()) -> |9|()
    29: +(|2|(),|8|()) -> c(|1|(),|0|())
    30: +(|2|(),|9|()) -> c(|1|(),|1|())
    31: +(|3|(),|0|()) -> |3|()
    32: +(|3|(),|1|()) -> |4|()
    33: +(|3|(),|2|()) -> |5|()
    34: +(|3|(),|3|()) -> |6|()
    35: +(|3|(),|4|()) -> |7|()
    36: +(|3|(),|5|()) -> |8|()
    37: +(|3|(),|6|()) -> |9|()
    38: +(|3|(),|7|()) -> c(|1|(),|0|())
    39: +(|3|(),|8|()) -> c(|1|(),|1|())
    40: +(|3|(),|9|()) -> c(|1|(),|2|())
    41: +(|4|(),|0|()) -> |4|()
    42: +(|4|(),|1|()) -> |5|()
    43: +(|4|(),|2|()) -> |6|()
    44: +(|4|(),|3|()) -> |7|()
    45: +(|4|(),|4|()) -> |8|()
    46: +(|4|(),|5|()) -> |9|()
    47: +(|4|(),|6|()) -> c(|1|(),|0|())
    48: +(|4|(),|7|()) -> c(|1|(),|1|())
    49: +(|4|(),|8|()) -> c(|1|(),|2|())
    50: +(|4|(),|9|()) -> c(|1|(),|3|())
    51: +(|5|(),|0|()) -> |5|()
    52: +(|5|(),|1|()) -> |6|()
    53: +(|5|(),|2|()) -> |7|()
    54: +(|5|(),|3|()) -> |8|()
    55: +(|5|(),|4|()) -> |9|()
    56: +(|5|(),|5|()) -> c(|1|(),|0|())
    57: +(|5|(),|6|()) -> c(|1|(),|1|())
    58: +(|5|(),|7|()) -> c(|1|(),|2|())
    59: +(|5|(),|8|()) -> c(|1|(),|3|())
    60: +(|5|(),|9|()) -> c(|1|(),|4|())
    61: +(|6|(),|0|()) -> |6|()
    62: +(|6|(),|1|()) -> |7|()
    63: +(|6|(),|2|()) -> |8|()
    64: +(|6|(),|3|()) -> |9|()
    65: +(|6|(),|4|()) -> c(|1|(),|0|())
    66: +(|6|(),|5|()) -> c(|1|(),|1|())
    67: +(|6|(),|6|()) -> c(|1|(),|2|())
    68: +(|6|(),|7|()) -> c(|1|(),|3|())
    69: +(|6|(),|8|()) -> c(|1|(),|4|())
    70: +(|6|(),|9|()) -> c(|1|(),|5|())
    71: +(|7|(),|0|()) -> |7|()
    72: +(|7|(),|1|()) -> |8|()
    73: +(|7|(),|2|()) -> |9|()
    74: +(|7|(),|3|()) -> c(|1|(),|0|())
    75: +(|7|(),|4|()) -> c(|1|(),|1|())
    76: +(|7|(),|5|()) -> c(|1|(),|2|())
    77: +(|7|(),|6|()) -> c(|1|(),|3|())
    78: +(|7|(),|7|()) -> c(|1|(),|4|())
    79: +(|7|(),|8|()) -> c(|1|(),|5|())
    80: +(|7|(),|9|()) -> c(|1|(),|6|())
    81: +(|8|(),|0|()) -> |8|()
    82: +(|8|(),|1|()) -> |9|()
    83: +(|8|(),|2|()) -> c(|1|(),|0|())
    84: +(|8|(),|3|()) -> c(|1|(),|1|())
    85: +(|8|(),|4|()) -> c(|1|(),|2|())
    86: +(|8|(),|5|()) -> c(|1|(),|3|())
    87: +(|8|(),|6|()) -> c(|1|(),|4|())
    88: +(|8|(),|7|()) -> c(|1|(),|5|())
    89: +(|8|(),|8|()) -> c(|1|(),|6|())
    90: +(|8|(),|9|()) -> c(|1|(),|7|())
    91: +(|9|(),|0|()) -> |9|()
    92: +(|9|(),|1|()) -> c(|1|(),|0|())
    93: +(|9|(),|2|()) -> c(|1|(),|1|())
    94: +(|9|(),|3|()) -> c(|1|(),|2|())
    95: +(|9|(),|4|()) -> c(|1|(),|3|())
    96: +(|9|(),|5|()) -> c(|1|(),|4|())
    97: +(|9|(),|6|()) -> c(|1|(),|5|())
    98: +(|9|(),|7|()) -> c(|1|(),|6|())
    99: +(|9|(),|8|()) -> c(|1|(),|7|())
    100: +(|9|(),|9|()) -> c(|1|(),|8|())
    101: +(x,c(y,z)) -> c(y,+(x,z))
    102: +(c(x,y),z) -> c(x,+(y,z))
    103: c(|0|(),x) -> x
    104: c(x,c(y,z)) -> c(+(x,y),z)
Number of strict rules: 104
Direct Order(PosReal,>,Poly) ... removes: 18 4 103 15 8 54 1 3 16 21 36 26 63 19 32 17 27 34 22 28 44 5 72 33 64 10 7 25 52 62 14 82 31 12 45 81 23 24 11 9 13 51 55 6 61 71 53 73 91 37 41 42 46 35 43 2
   |0|()	weight: 0
   |8|()	weight: 0
     c(x1,x2)	weight: (/ 1 4) + x1 + x2
   |6|()	weight: 0
   |9|()	weight: 0
   |7|()	weight: 0
   |4|()	weight: 0
   |1|()	weight: 0
   |5|()	weight: 0
   |3|()	weight: 0
   |2|()	weight: 0
     +(x1,x2)	weight: (/ 1 4) + x1 + x2
Number of strict rules: 48
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #+(|8|(),|5|()) -> #c(|1|(),|3|())
   #2: #+(|2|(),|8|()) -> #c(|1|(),|0|())
   #3: #+(|8|(),|2|()) -> #c(|1|(),|0|())
   #4: #+(|6|(),|5|()) -> #c(|1|(),|1|())
   #5: #+(|9|(),|4|()) -> #c(|1|(),|3|())
   #6: #+(|9|(),|8|()) -> #c(|1|(),|7|())
   #7: #+(|9|(),|6|()) -> #c(|1|(),|5|())
   #8: #+(|4|(),|6|()) -> #c(|1|(),|0|())
   #9: #+(|4|(),|7|()) -> #c(|1|(),|1|())
   #10: #+(|7|(),|4|()) -> #c(|1|(),|1|())
   #11: #+(|7|(),|3|()) -> #c(|1|(),|0|())
   #12: #+(|5|(),|7|()) -> #c(|1|(),|2|())
   #13: #+(|3|(),|7|()) -> #c(|1|(),|0|())
   #14: #+(|5|(),|8|()) -> #c(|1|(),|3|())
   #15: #+(|6|(),|6|()) -> #c(|1|(),|2|())
   #16: #+(|3|(),|9|()) -> #c(|1|(),|2|())
   #17: #+(|8|(),|9|()) -> #c(|1|(),|7|())
   #18: #+(|9|(),|7|()) -> #c(|1|(),|6|())
   #19: #+(|5|(),|6|()) -> #c(|1|(),|1|())
   #20: #+(|7|(),|5|()) -> #c(|1|(),|2|())
   #21: #+(|9|(),|3|()) -> #c(|1|(),|2|())
   #22: #+(|6|(),|9|()) -> #c(|1|(),|5|())
   #23: #+(|7|(),|7|()) -> #c(|1|(),|4|())
   #24: #+(|9|(),|5|()) -> #c(|1|(),|4|())
   #25: #+(|6|(),|8|()) -> #c(|1|(),|4|())
   #26: #+(x,c(y,z)) -> #c(y,+(x,z))
   #27: #+(x,c(y,z)) -> #+(x,z)
   #28: #+(|7|(),|8|()) -> #c(|1|(),|5|())
   #29: #+(|5|(),|5|()) -> #c(|1|(),|0|())
   #30: #+(|8|(),|8|()) -> #c(|1|(),|6|())
   #31: #+(|2|(),|9|()) -> #c(|1|(),|1|())
   #32: #+(|4|(),|8|()) -> #c(|1|(),|2|())
   #33: #+(|1|(),|9|()) -> #c(|1|(),|0|())
   #34: #+(|8|(),|7|()) -> #c(|1|(),|5|())
   #35: #+(|3|(),|8|()) -> #c(|1|(),|1|())
   #36: #+(|9|(),|1|()) -> #c(|1|(),|0|())
   #37: #+(|9|(),|2|()) -> #c(|1|(),|1|())
   #38: #+(|6|(),|4|()) -> #c(|1|(),|0|())
   #39: #+(|8|(),|3|()) -> #c(|1|(),|1|())
   #40: #+(|8|(),|6|()) -> #c(|1|(),|4|())
   #41: #+(|5|(),|9|()) -> #c(|1|(),|4|())
   #42: #+(|9|(),|9|()) -> #c(|1|(),|8|())
   #43: #+(|8|(),|4|()) -> #c(|1|(),|2|())
   #44: #+(|6|(),|7|()) -> #c(|1|(),|3|())
   #45: #+(|7|(),|6|()) -> #c(|1|(),|3|())
   #46: #+(c(x,y),z) -> #c(x,+(y,z))
   #47: #+(c(x,y),z) -> #+(y,z)
   #48: #c(x,c(y,z)) -> #c(+(x,y),z)
   #49: #c(x,c(y,z)) -> #+(x,y)
   #50: #+(|7|(),|9|()) -> #c(|1|(),|6|())
   #51: #+(|4|(),|9|()) -> #c(|1|(),|3|())
Number of SCCs: 1, DPs: 6, edges: 18
	SCC { #26 #27 #46..49 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
   |8|()	weight: 0
     c(x1,x2)	weight: (/ 1 2) + x1 + x2
   |6|()	weight: 0
   |9|()	weight: 0
   |7|()	weight: 0
   |4|()	weight: 0
   |1|()	weight: 0
   |5|()	weight: 0
   |3|()	weight: 0
   #c(x1,x2)	weight: x1 + x2
   |2|()	weight: 0
     +(x1,x2)	weight: (/ 1 2) + x1 + x2
   #+(x1,x2)	weight: (/ 1 4) + x1 + x2
    Usable rules: { 20 29 30 38..40 47..50 56..60 65..70 74..80 83..90 92..102 104 }
    Removed DPs: #26 #27 #46 #47 #49
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #48 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
   |8|()	weight: 0
     c(x1,x2)	weight: (/ 1 2) + x1 + x2
   |6|()	weight: 0
   |9|()	weight: 0
   |7|()	weight: 0
   |4|()	weight: 0
   |1|()	weight: 0
   |5|()	weight: 0
   |3|()	weight: 0
   #c(x1,x2)	weight: x2
   |2|()	weight: 0
     +(x1,x2)	weight: (/ 1 2) + x1 + x2
   #+(x1,x2)	weight: (/ 1 4)
    Usable rules: { 20 29 30 38..40 47..50 56..60 65..70 74..80 83..90 92..102 104 }
    Removed DPs: #48
Number of SCCs: 0, DPs: 0, edges: 0
YES