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 7() weight: 0 1() weight: 0 4() weight: 0 5() weight: 0 3() weight: 0 c(x1,x2) weight: 32286 + x1 + x2 9() weight: 0 8() weight: 0 0() weight: 0 2() weight: 0 6() weight: 0 +(x1,x2) weight: 32286 + 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. 7() weight: 0 1() weight: 0 4() weight: 0 5() weight: 0 3() weight: 0 c(x1,x2) weight: (/ 1 2) + x1 + x2 9() weight: 0 8() weight: 0 0() weight: 0 #c(x1,x2) weight: x1 + x2 2() weight: 0 6() 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. 7() weight: 0 1() weight: 0 4() weight: 0 5() weight: 0 3() weight: 0 c(x1,x2) weight: (/ 1 2) + x1 + x2 9() weight: 0 8() weight: 0 0() weight: 0 #c(x1,x2) weight: x2 2() weight: 0 6() weight: 0 +(x1,x2) weight: (/ 1 2) + x1 + x2 #+(x1,x2) weight: (/ 1 2) 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