Input TRS: 1: active(from(X)) -> mark(cons(X,from(s(X)))) 2: active(|2ndspos|(|0|(),Z)) -> mark(rnil()) 3: active(|2ndspos|(s(N),cons(X,cons(Y,Z)))) -> mark(rcons(posrecip(Y),|2ndsneg|(N,Z))) 4: active(|2ndsneg|(|0|(),Z)) -> mark(rnil()) 5: active(|2ndsneg|(s(N),cons(X,cons(Y,Z)))) -> mark(rcons(negrecip(Y),|2ndspos|(N,Z))) 6: active(pi(X)) -> mark(|2ndspos|(X,from(|0|()))) 7: active(plus(|0|(),Y)) -> mark(Y) 8: active(plus(s(X),Y)) -> mark(s(plus(X,Y))) 9: active(times(|0|(),Y)) -> mark(|0|()) 10: active(times(s(X),Y)) -> mark(plus(Y,times(X,Y))) 11: active(square(X)) -> mark(times(X,X)) 12: mark(from(X)) -> active(from(mark(X))) 13: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 14: mark(s(X)) -> active(s(mark(X))) 15: mark(|2ndspos|(X1,X2)) -> active(|2ndspos|(mark(X1),mark(X2))) 16: mark(|0|()) -> active(|0|()) 17: mark(rnil()) -> active(rnil()) 18: mark(rcons(X1,X2)) -> active(rcons(mark(X1),mark(X2))) 19: mark(posrecip(X)) -> active(posrecip(mark(X))) 20: mark(|2ndsneg|(X1,X2)) -> active(|2ndsneg|(mark(X1),mark(X2))) 21: mark(negrecip(X)) -> active(negrecip(mark(X))) 22: mark(pi(X)) -> active(pi(mark(X))) 23: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) 24: mark(times(X1,X2)) -> active(times(mark(X1),mark(X2))) 25: mark(square(X)) -> active(square(mark(X))) 26: from(mark(X)) -> from(X) 27: from(active(X)) -> from(X) 28: cons(mark(X1),X2) -> cons(X1,X2) 29: cons(X1,mark(X2)) -> cons(X1,X2) 30: cons(active(X1),X2) -> cons(X1,X2) 31: cons(X1,active(X2)) -> cons(X1,X2) 32: s(mark(X)) -> s(X) 33: s(active(X)) -> s(X) 34: |2ndspos|(mark(X1),X2) -> |2ndspos|(X1,X2) 35: |2ndspos|(X1,mark(X2)) -> |2ndspos|(X1,X2) 36: |2ndspos|(active(X1),X2) -> |2ndspos|(X1,X2) 37: |2ndspos|(X1,active(X2)) -> |2ndspos|(X1,X2) 38: rcons(mark(X1),X2) -> rcons(X1,X2) 39: rcons(X1,mark(X2)) -> rcons(X1,X2) 40: rcons(active(X1),X2) -> rcons(X1,X2) 41: rcons(X1,active(X2)) -> rcons(X1,X2) 42: posrecip(mark(X)) -> posrecip(X) 43: posrecip(active(X)) -> posrecip(X) 44: |2ndsneg|(mark(X1),X2) -> |2ndsneg|(X1,X2) 45: |2ndsneg|(X1,mark(X2)) -> |2ndsneg|(X1,X2) 46: |2ndsneg|(active(X1),X2) -> |2ndsneg|(X1,X2) 47: |2ndsneg|(X1,active(X2)) -> |2ndsneg|(X1,X2) 48: negrecip(mark(X)) -> negrecip(X) 49: negrecip(active(X)) -> negrecip(X) 50: pi(mark(X)) -> pi(X) 51: pi(active(X)) -> pi(X) 52: plus(mark(X1),X2) -> plus(X1,X2) 53: plus(X1,mark(X2)) -> plus(X1,X2) 54: plus(active(X1),X2) -> plus(X1,X2) 55: plus(X1,active(X2)) -> plus(X1,X2) 56: times(mark(X1),X2) -> times(X1,X2) 57: times(X1,mark(X2)) -> times(X1,X2) 58: times(active(X1),X2) -> times(X1,X2) 59: times(X1,active(X2)) -> times(X1,X2) 60: square(mark(X)) -> square(X) 61: square(active(X)) -> square(X) Number of strict rules: 61 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #active(|2ndspos|(|0|(),Z)) -> #mark(rnil()) #2: #posrecip(active(X)) -> #posrecip(X) #3: #cons(X1,mark(X2)) -> #cons(X1,X2) #4: #|2ndspos|(X1,mark(X2)) -> #|2ndspos|(X1,X2) #5: #|2ndsneg|(active(X1),X2) -> #|2ndsneg|(X1,X2) #6: #posrecip(mark(X)) -> #posrecip(X) #7: #rcons(X1,active(X2)) -> #rcons(X1,X2) #8: #|2ndspos|(X1,active(X2)) -> #|2ndspos|(X1,X2) #9: #|2ndsneg|(X1,active(X2)) -> #|2ndsneg|(X1,X2) #10: #plus(X1,mark(X2)) -> #plus(X1,X2) #11: #negrecip(mark(X)) -> #negrecip(X) #12: #times(active(X1),X2) -> #times(X1,X2) #13: #square(active(X)) -> #square(X) #14: #rcons(mark(X1),X2) -> #rcons(X1,X2) #15: #active(pi(X)) -> #mark(|2ndspos|(X,from(|0|()))) #16: #active(pi(X)) -> #|2ndspos|(X,from(|0|())) #17: #active(pi(X)) -> #from(|0|()) #18: #times(X1,active(X2)) -> #times(X1,X2) #19: #plus(X1,active(X2)) -> #plus(X1,X2) #20: #rcons(active(X1),X2) -> #rcons(X1,X2) #21: #pi(active(X)) -> #pi(X) #22: #mark(cons(X1,X2)) -> #active(cons(mark(X1),X2)) #23: #mark(cons(X1,X2)) -> #cons(mark(X1),X2) #24: #mark(cons(X1,X2)) -> #mark(X1) #25: #active(times(|0|(),Y)) -> #mark(|0|()) #26: #active(square(X)) -> #mark(times(X,X)) #27: #active(square(X)) -> #times(X,X) #28: #times(X1,mark(X2)) -> #times(X1,X2) #29: #mark(times(X1,X2)) -> #active(times(mark(X1),mark(X2))) #30: #mark(times(X1,X2)) -> #times(mark(X1),mark(X2)) #31: #mark(times(X1,X2)) -> #mark(X1) #32: #mark(times(X1,X2)) -> #mark(X2) #33: #mark(plus(X1,X2)) -> #active(plus(mark(X1),mark(X2))) #34: #mark(plus(X1,X2)) -> #plus(mark(X1),mark(X2)) #35: #mark(plus(X1,X2)) -> #mark(X1) #36: #mark(plus(X1,X2)) -> #mark(X2) #37: #|2ndsneg|(X1,mark(X2)) -> #|2ndsneg|(X1,X2) #38: #mark(from(X)) -> #active(from(mark(X))) #39: #mark(from(X)) -> #from(mark(X)) #40: #mark(from(X)) -> #mark(X) #41: #cons(X1,active(X2)) -> #cons(X1,X2) #42: #times(mark(X1),X2) -> #times(X1,X2) #43: #mark(s(X)) -> #active(s(mark(X))) #44: #mark(s(X)) -> #s(mark(X)) #45: #mark(s(X)) -> #mark(X) #46: #cons(active(X1),X2) -> #cons(X1,X2) #47: #plus(mark(X1),X2) -> #plus(X1,X2) #48: #negrecip(active(X)) -> #negrecip(X) #49: #mark(square(X)) -> #active(square(mark(X))) #50: #mark(square(X)) -> #square(mark(X)) #51: #mark(square(X)) -> #mark(X) #52: #mark(|2ndsneg|(X1,X2)) -> #active(|2ndsneg|(mark(X1),mark(X2))) #53: #mark(|2ndsneg|(X1,X2)) -> #|2ndsneg|(mark(X1),mark(X2)) #54: #mark(|2ndsneg|(X1,X2)) -> #mark(X1) #55: #mark(|2ndsneg|(X1,X2)) -> #mark(X2) #56: #active(plus(|0|(),Y)) -> #mark(Y) #57: #rcons(X1,mark(X2)) -> #rcons(X1,X2) #58: #active(times(s(X),Y)) -> #mark(plus(Y,times(X,Y))) #59: #active(times(s(X),Y)) -> #plus(Y,times(X,Y)) #60: #active(times(s(X),Y)) -> #times(X,Y) #61: #s(active(X)) -> #s(X) #62: #active(|2ndsneg|(s(N),cons(X,cons(Y,Z)))) -> #mark(rcons(negrecip(Y),|2ndspos|(N,Z))) #63: #active(|2ndsneg|(s(N),cons(X,cons(Y,Z)))) -> #rcons(negrecip(Y),|2ndspos|(N,Z)) #64: #active(|2ndsneg|(s(N),cons(X,cons(Y,Z)))) -> #negrecip(Y) #65: #active(|2ndsneg|(s(N),cons(X,cons(Y,Z)))) -> #|2ndspos|(N,Z) #66: #|2ndsneg|(mark(X1),X2) -> #|2ndsneg|(X1,X2) #67: #cons(mark(X1),X2) -> #cons(X1,X2) #68: #mark(pi(X)) -> #active(pi(mark(X))) #69: #mark(pi(X)) -> #pi(mark(X)) #70: #mark(pi(X)) -> #mark(X) #71: #|2ndspos|(mark(X1),X2) -> #|2ndspos|(X1,X2) #72: #from(active(X)) -> #from(X) #73: #square(mark(X)) -> #square(X) #74: #mark(rnil()) -> #active(rnil()) #75: #s(mark(X)) -> #s(X) #76: #mark(posrecip(X)) -> #active(posrecip(mark(X))) #77: #mark(posrecip(X)) -> #posrecip(mark(X)) #78: #mark(posrecip(X)) -> #mark(X) #79: #from(mark(X)) -> #from(X) #80: #|2ndspos|(active(X1),X2) -> #|2ndspos|(X1,X2) #81: #mark(negrecip(X)) -> #active(negrecip(mark(X))) #82: #mark(negrecip(X)) -> #negrecip(mark(X)) #83: #mark(negrecip(X)) -> #mark(X) #84: #mark(|0|()) -> #active(|0|()) #85: #active(|2ndspos|(s(N),cons(X,cons(Y,Z)))) -> #mark(rcons(posrecip(Y),|2ndsneg|(N,Z))) #86: #active(|2ndspos|(s(N),cons(X,cons(Y,Z)))) -> #rcons(posrecip(Y),|2ndsneg|(N,Z)) #87: #active(|2ndspos|(s(N),cons(X,cons(Y,Z)))) -> #posrecip(Y) #88: #active(|2ndspos|(s(N),cons(X,cons(Y,Z)))) -> #|2ndsneg|(N,Z) #89: #active(from(X)) -> #mark(cons(X,from(s(X)))) #90: #active(from(X)) -> #cons(X,from(s(X))) #91: #active(from(X)) -> #from(s(X)) #92: #active(from(X)) -> #s(X) #93: #plus(active(X1),X2) -> #plus(X1,X2) #94: #active(plus(s(X),Y)) -> #mark(s(plus(X,Y))) #95: #active(plus(s(X),Y)) -> #s(plus(X,Y)) #96: #active(plus(s(X),Y)) -> #plus(X,Y) #97: #mark(|2ndspos|(X1,X2)) -> #active(|2ndspos|(mark(X1),mark(X2))) #98: #mark(|2ndspos|(X1,X2)) -> #|2ndspos|(mark(X1),mark(X2)) #99: #mark(|2ndspos|(X1,X2)) -> #mark(X1) #100: #mark(|2ndspos|(X1,X2)) -> #mark(X2) #101: #active(|2ndsneg|(|0|(),Z)) -> #mark(rnil()) #102: #pi(mark(X)) -> #pi(X) #103: #mark(rcons(X1,X2)) -> #active(rcons(mark(X1),mark(X2))) #104: #mark(rcons(X1,X2)) -> #rcons(mark(X1),mark(X2)) #105: #mark(rcons(X1,X2)) -> #mark(X1) #106: #mark(rcons(X1,X2)) -> #mark(X2) Number of SCCs: 13, DPs: 68, edges: 575 SCC { #2 #6 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: x1 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #2 #6 Number of SCCs: 12, DPs: 66, edges: 571 SCC { #11 #48 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: x1 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #11 #48 Number of SCCs: 11, DPs: 64, edges: 567 SCC { #21 #102 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: x1 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #21 #102 Number of SCCs: 10, DPs: 62, edges: 563 SCC { #13 #73 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: x1 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #13 #73 Number of SCCs: 9, DPs: 60, edges: 559 SCC { #61 #75 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: x1 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #61 #75 Number of SCCs: 8, DPs: 58, edges: 555 SCC { #72 #79 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: x1 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #72 #79 Number of SCCs: 7, DPs: 56, edges: 551 SCC { #7 #14 #20 #57 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: x2 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #7 #57 Number of SCCs: 7, DPs: 54, edges: 539 SCC { #14 #20 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: x1 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #14 #20 Number of SCCs: 6, DPs: 52, edges: 535 SCC { #12 #18 #28 #42 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: x2 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #18 #28 Number of SCCs: 7, DPs: 50, edges: 523 SCC { #12 #42 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: x1 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #12 #42 Number of SCCs: 6, DPs: 48, edges: 519 SCC { #10 #19 #47 #93 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: x1 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #47 #93 Number of SCCs: 7, DPs: 46, edges: 507 SCC { #10 #19 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: x2 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #10 #19 Number of SCCs: 6, DPs: 44, edges: 503 SCC { #4 #8 #71 #80 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: x2 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #4 #8 Number of SCCs: 7, DPs: 42, edges: 491 SCC { #71 #80 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: x1 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #71 #80 Number of SCCs: 6, DPs: 40, edges: 487 SCC { #5 #9 #37 #66 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: x2 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #9 #37 Number of SCCs: 7, DPs: 38, edges: 475 SCC { #5 #66 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: x1 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #5 #66 Number of SCCs: 6, DPs: 36, edges: 471 SCC { #3 #41 #46 #67 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: x2 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #3 #41 Number of SCCs: 7, DPs: 34, edges: 459 SCC { #46 #67 } Removing DPs: Order(PosReal,>,Sum)... succeeded. |0|() weight: 0 negrecip(x1) weight: 0 #cons(x1,x2) weight: x1 s(x1) weight: 0 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: 0 #plus(x1,x2) weight: 0 square(x1) weight: 0 #square(x1) weight: 0 pi(x1) weight: 0 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: 0 |2ndsneg|(x1,x2) weight: 0 #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: 0 #posrecip(x1) weight: 0 from(x1) weight: 0 times(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #from(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #pi(x1) weight: 0 posrecip(x1) weight: 0 Usable rules: { } Removed DPs: #46 #67 Number of SCCs: 6, DPs: 32, edges: 455 SCC { #15 #24 #26 #29 #31..33 #35 #36 #38 #40 #45 #49 #51 #52 #54..56 #58 #62 #68 #70 #78 #83 #85 #89 #94 #97 #99 #100 #105 #106 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. |0|() weight: (/ 1 4) negrecip(x1) weight: (/ 1 4) + x1 #cons(x1,x2) weight: 0 s(x1) weight: x1 #negrecip(x1) weight: 0 rnil() weight: 0 |2ndspos|(x1,x2) weight: max{(/ 193 4) + x2, (/ 1127 4) + x1} #plus(x1,x2) weight: 0 square(x1) weight: 17064 + x1 #square(x1) weight: 0 pi(x1) weight: (/ 1129 4) + x1 #rcons(x1,x2) weight: 0 rcons(x1,x2) weight: max{x2, (/ 1125 4) + x1} |2ndsneg|(x1,x2) weight: max{(/ 193 4) + x2, (/ 1127 4) + x1} #|2ndspos|(x1,x2) weight: 0 #|2ndsneg|(x1,x2) weight: 0 #times(x1,x2) weight: 0 #mark(x1) weight: x1 #posrecip(x1) weight: 0 from(x1) weight: (/ 467 2) + x1 times(x1,x2) weight: max{(/ 34127 2) + x2, (/ 68255 4) + x1} #s(x1) weight: 0 mark(x1) weight: x1 plus(x1,x2) weight: max{x2, (/ 68253 4) + x1} #from(x1) weight: 0 active(x1) weight: x1 cons(x1,x2) weight: max{x2, (/ 933 4) + x1} #active(x1) weight: x1 #pi(x1) weight: 0 posrecip(x1) weight: (/ 1 4) + x1 Usable rules: { 1..61 } Removed DPs: #15 #24 #26 #31 #32 #35 #40 #51 #54 #55 #70 #78 #83 #99 #100 #105 Number of SCCs: 7, DPs: 12, edges: 38 SCC { #29 #33 #36 #45 #52 #56 #58 #62 #85 #94 #97 #106 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded. |0|() status: [] precedence above: negrecip(x1) status: [] precedence above: s rnil |2ndspos| |2ndsneg| active cons posrecip #cons(x1,x2) status: [] precedence above: s(x1) status: [x1] precedence above: negrecip rnil |2ndspos| |2ndsneg| active cons posrecip #negrecip(x1) status: [] precedence above: rnil() status: [] precedence above: |2ndspos|(x1,x2) status: [x2] precedence above: negrecip s rnil |2ndsneg| active cons posrecip #plus(x1,x2) status: [] precedence above: square(x1) status: [x1] precedence above: |0| negrecip s rnil |2ndspos| |2ndsneg| #mark times mark plus active cons #active posrecip #square(x1) status: [] precedence above: pi(x1) status: [] precedence above: negrecip s rnil |2ndspos| |2ndsneg| from mark active cons posrecip #rcons(x1,x2) status: [x1,x2] precedence above: rcons(x1,x2) status: x2 |2ndsneg|(x1,x2) status: [x2] precedence above: negrecip s rnil |2ndspos| active cons posrecip #|2ndspos|(x1,x2) status: [x1] precedence above: #|2ndsneg|(x1,x2) status: [x2] precedence above: #times(x1,x2) status: [x1,x2] precedence above: #mark(x1) status: [x1] precedence above: negrecip s rnil |2ndspos| |2ndsneg| active cons #active posrecip #posrecip(x1) status: [] precedence above: from(x1) status: [] precedence above: cons times(x1,x2) status: [x1,x2] precedence above: |0| negrecip s rnil |2ndspos| |2ndsneg| #mark mark plus active cons #active posrecip #s(x1) status: [] precedence above: mark(x1) status: x1 plus(x1,x2) status: [x2,x1] precedence above: negrecip s rnil |2ndspos| |2ndsneg| #mark mark active cons #active posrecip #from(x1) status: [] precedence above: active(x1) status: x1 cons(x1,x2) status: x2 #active(x1) status: [x1] precedence above: negrecip s rnil |2ndspos| |2ndsneg| #mark active cons posrecip #pi(x1) status: [] precedence above: posrecip(x1) status: [] precedence above: negrecip s rnil |2ndspos| |2ndsneg| active cons Usable rules: { 1..61 } Removed DPs: #36 #45 #56 #58 #94 Number of SCCs: 7, DPs: 5, edges: 7 SCC { #52 #62 #85 #97 #106 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded. |0|() status: [] precedence above: rnil negrecip(x1) status: [] precedence above: s rnil |2ndspos| rcons |2ndsneg| #mark cons #active posrecip #cons(x1,x2) status: [] precedence above: s(x1) status: [x1] precedence above: negrecip rnil |2ndspos| rcons |2ndsneg| #mark cons #active posrecip #negrecip(x1) status: [] precedence above: rnil() status: [] precedence above: |2ndspos|(x1,x2) status: [x2,x1] precedence above: rnil rcons |2ndsneg| #mark #active #plus(x1,x2) status: [] precedence above: square(x1) status: [x1] precedence above: |0| negrecip s rnil |2ndspos| pi rcons |2ndsneg| #mark from times mark plus active cons #active posrecip #square(x1) status: [] precedence above: pi(x1) status: [x1] precedence above: rnil |2ndspos| rcons |2ndsneg| #mark from mark #active #rcons(x1,x2) status: [x1,x2] precedence above: rcons(x1,x2) status: [x1,x2] precedence above: rnil #mark #active |2ndsneg|(x1,x2) status: [x2,x1] precedence above: rnil |2ndspos| rcons #mark #active #|2ndspos|(x1,x2) status: [x1] precedence above: #|2ndsneg|(x1,x2) status: [x2] precedence above: #times(x1,x2) status: [x1,x2] precedence above: #mark(x1) status: [x1] precedence above: rnil rcons #active #posrecip(x1) status: [] precedence above: from(x1) status: [] precedence above: times(x1,x2) status: [x1,x2] precedence above: |0| negrecip s rnil |2ndspos| pi rcons |2ndsneg| #mark from mark plus active cons #active posrecip #s(x1) status: [] precedence above: mark(x1) status: x1 plus(x1,x2) status: [x1,x2] precedence above: negrecip s rnil |2ndspos| pi rcons |2ndsneg| #mark from mark active cons #active posrecip #from(x1) status: [] precedence above: active(x1) status: x1 cons(x1,x2) status: x2 #active(x1) status: [x1] precedence above: rnil rcons #mark #pi(x1) status: [] precedence above: posrecip(x1) status: [] precedence above: negrecip s rnil |2ndspos| rcons |2ndsneg| #mark cons #active Usable rules: { 1..61 } Removed DPs: #62 #106 Number of SCCs: 6, DPs: 0, edges: 0 YES