Input TRS: 1: active(U101(tt(),N,XS)) -> mark(fst(splitAt(N,XS))) 2: active(U11(tt(),N,XS)) -> mark(snd(splitAt(N,XS))) 3: active(U21(tt(),X)) -> mark(X) 4: active(U31(tt(),N)) -> mark(N) 5: active(U41(tt(),N)) -> mark(cons(N,natsFrom(s(N)))) 6: active(U51(tt(),N,XS)) -> mark(head(afterNth(N,XS))) 7: active(U61(tt(),Y)) -> mark(Y) 8: active(U71(tt(),XS)) -> mark(pair(nil(),XS)) 9: active(U81(tt(),N,X,XS)) -> mark(U82(splitAt(N,XS),X)) 10: active(U82(pair(YS,ZS),X)) -> mark(pair(cons(X,YS),ZS)) 11: active(U91(tt(),XS)) -> mark(XS) 12: active(afterNth(N,XS)) -> mark(U11(and(isNatural(N),isLNat(XS)),N,XS)) 13: active(and(tt(),X)) -> mark(X) 14: active(fst(pair(X,Y))) -> mark(U21(and(isLNat(X),isLNat(Y)),X)) 15: active(head(cons(N,XS))) -> mark(U31(and(isNatural(N),isLNat(XS)),N)) 16: active(isLNat(nil())) -> mark(tt()) 17: active(isLNat(afterNth(V1,V2))) -> mark(and(isNatural(V1),isLNat(V2))) 18: active(isLNat(cons(V1,V2))) -> mark(and(isNatural(V1),isLNat(V2))) 19: active(isLNat(fst(V1))) -> mark(isPLNat(V1)) 20: active(isLNat(natsFrom(V1))) -> mark(isNatural(V1)) 21: active(isLNat(snd(V1))) -> mark(isPLNat(V1)) 22: active(isLNat(tail(V1))) -> mark(isLNat(V1)) 23: active(isLNat(take(V1,V2))) -> mark(and(isNatural(V1),isLNat(V2))) 24: active(isNatural(0())) -> mark(tt()) 25: active(isNatural(head(V1))) -> mark(isLNat(V1)) 26: active(isNatural(s(V1))) -> mark(isNatural(V1)) 27: active(isNatural(sel(V1,V2))) -> mark(and(isNatural(V1),isLNat(V2))) 28: active(isPLNat(pair(V1,V2))) -> mark(and(isLNat(V1),isLNat(V2))) 29: active(isPLNat(splitAt(V1,V2))) -> mark(and(isNatural(V1),isLNat(V2))) 30: active(natsFrom(N)) -> mark(U41(isNatural(N),N)) 31: active(sel(N,XS)) -> mark(U51(and(isNatural(N),isLNat(XS)),N,XS)) 32: active(snd(pair(X,Y))) -> mark(U61(and(isLNat(X),isLNat(Y)),Y)) 33: active(splitAt(0(),XS)) -> mark(U71(isLNat(XS),XS)) 34: active(splitAt(s(N),cons(X,XS))) -> mark(U81(and(isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS)) 35: active(tail(cons(N,XS))) -> mark(U91(and(isNatural(N),isLNat(XS)),XS)) 36: active(take(N,XS)) -> mark(U101(and(isNatural(N),isLNat(XS)),N,XS)) 37: mark(U101(X1,X2,X3)) -> active(U101(mark(X1),X2,X3)) 38: mark(tt()) -> active(tt()) 39: mark(fst(X)) -> active(fst(mark(X))) 40: mark(splitAt(X1,X2)) -> active(splitAt(mark(X1),mark(X2))) 41: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3)) 42: mark(snd(X)) -> active(snd(mark(X))) 43: mark(U21(X1,X2)) -> active(U21(mark(X1),X2)) 44: mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) 45: mark(U41(X1,X2)) -> active(U41(mark(X1),X2)) 46: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 47: mark(natsFrom(X)) -> active(natsFrom(mark(X))) 48: mark(s(X)) -> active(s(mark(X))) 49: mark(U51(X1,X2,X3)) -> active(U51(mark(X1),X2,X3)) 50: mark(head(X)) -> active(head(mark(X))) 51: mark(afterNth(X1,X2)) -> active(afterNth(mark(X1),mark(X2))) 52: mark(U61(X1,X2)) -> active(U61(mark(X1),X2)) 53: mark(U71(X1,X2)) -> active(U71(mark(X1),X2)) 54: mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2))) 55: mark(nil()) -> active(nil()) 56: mark(U81(X1,X2,X3,X4)) -> active(U81(mark(X1),X2,X3,X4)) 57: mark(U82(X1,X2)) -> active(U82(mark(X1),X2)) 58: mark(U91(X1,X2)) -> active(U91(mark(X1),X2)) 59: mark(and(X1,X2)) -> active(and(mark(X1),X2)) 60: mark(isNatural(X)) -> active(isNatural(X)) 61: mark(isLNat(X)) -> active(isLNat(X)) 62: mark(isPLNat(X)) -> active(isPLNat(X)) 63: mark(tail(X)) -> active(tail(mark(X))) 64: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2))) 65: mark(0()) -> active(0()) 66: mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2))) 67: U101(mark(X1),X2,X3) -> U101(X1,X2,X3) 68: U101(X1,mark(X2),X3) -> U101(X1,X2,X3) 69: U101(X1,X2,mark(X3)) -> U101(X1,X2,X3) 70: U101(active(X1),X2,X3) -> U101(X1,X2,X3) 71: U101(X1,active(X2),X3) -> U101(X1,X2,X3) 72: U101(X1,X2,active(X3)) -> U101(X1,X2,X3) 73: fst(mark(X)) -> fst(X) 74: fst(active(X)) -> fst(X) 75: splitAt(mark(X1),X2) -> splitAt(X1,X2) 76: splitAt(X1,mark(X2)) -> splitAt(X1,X2) 77: splitAt(active(X1),X2) -> splitAt(X1,X2) 78: splitAt(X1,active(X2)) -> splitAt(X1,X2) 79: U11(mark(X1),X2,X3) -> U11(X1,X2,X3) 80: U11(X1,mark(X2),X3) -> U11(X1,X2,X3) 81: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3) 82: U11(active(X1),X2,X3) -> U11(X1,X2,X3) 83: U11(X1,active(X2),X3) -> U11(X1,X2,X3) 84: U11(X1,X2,active(X3)) -> U11(X1,X2,X3) 85: snd(mark(X)) -> snd(X) 86: snd(active(X)) -> snd(X) 87: U21(mark(X1),X2) -> U21(X1,X2) 88: U21(X1,mark(X2)) -> U21(X1,X2) 89: U21(active(X1),X2) -> U21(X1,X2) 90: U21(X1,active(X2)) -> U21(X1,X2) 91: U31(mark(X1),X2) -> U31(X1,X2) 92: U31(X1,mark(X2)) -> U31(X1,X2) 93: U31(active(X1),X2) -> U31(X1,X2) 94: U31(X1,active(X2)) -> U31(X1,X2) 95: U41(mark(X1),X2) -> U41(X1,X2) 96: U41(X1,mark(X2)) -> U41(X1,X2) 97: U41(active(X1),X2) -> U41(X1,X2) 98: U41(X1,active(X2)) -> U41(X1,X2) 99: cons(mark(X1),X2) -> cons(X1,X2) 100: cons(X1,mark(X2)) -> cons(X1,X2) 101: cons(active(X1),X2) -> cons(X1,X2) 102: cons(X1,active(X2)) -> cons(X1,X2) 103: natsFrom(mark(X)) -> natsFrom(X) 104: natsFrom(active(X)) -> natsFrom(X) 105: s(mark(X)) -> s(X) 106: s(active(X)) -> s(X) 107: U51(mark(X1),X2,X3) -> U51(X1,X2,X3) 108: U51(X1,mark(X2),X3) -> U51(X1,X2,X3) 109: U51(X1,X2,mark(X3)) -> U51(X1,X2,X3) 110: U51(active(X1),X2,X3) -> U51(X1,X2,X3) 111: U51(X1,active(X2),X3) -> U51(X1,X2,X3) 112: U51(X1,X2,active(X3)) -> U51(X1,X2,X3) 113: head(mark(X)) -> head(X) 114: head(active(X)) -> head(X) 115: afterNth(mark(X1),X2) -> afterNth(X1,X2) 116: afterNth(X1,mark(X2)) -> afterNth(X1,X2) 117: afterNth(active(X1),X2) -> afterNth(X1,X2) 118: afterNth(X1,active(X2)) -> afterNth(X1,X2) 119: U61(mark(X1),X2) -> U61(X1,X2) 120: U61(X1,mark(X2)) -> U61(X1,X2) 121: U61(active(X1),X2) -> U61(X1,X2) 122: U61(X1,active(X2)) -> U61(X1,X2) 123: U71(mark(X1),X2) -> U71(X1,X2) 124: U71(X1,mark(X2)) -> U71(X1,X2) 125: U71(active(X1),X2) -> U71(X1,X2) 126: U71(X1,active(X2)) -> U71(X1,X2) 127: pair(mark(X1),X2) -> pair(X1,X2) 128: pair(X1,mark(X2)) -> pair(X1,X2) 129: pair(active(X1),X2) -> pair(X1,X2) 130: pair(X1,active(X2)) -> pair(X1,X2) 131: U81(mark(X1),X2,X3,X4) -> U81(X1,X2,X3,X4) 132: U81(X1,mark(X2),X3,X4) -> U81(X1,X2,X3,X4) 133: U81(X1,X2,mark(X3),X4) -> U81(X1,X2,X3,X4) 134: U81(X1,X2,X3,mark(X4)) -> U81(X1,X2,X3,X4) 135: U81(active(X1),X2,X3,X4) -> U81(X1,X2,X3,X4) 136: U81(X1,active(X2),X3,X4) -> U81(X1,X2,X3,X4) 137: U81(X1,X2,active(X3),X4) -> U81(X1,X2,X3,X4) 138: U81(X1,X2,X3,active(X4)) -> U81(X1,X2,X3,X4) 139: U82(mark(X1),X2) -> U82(X1,X2) 140: U82(X1,mark(X2)) -> U82(X1,X2) 141: U82(active(X1),X2) -> U82(X1,X2) 142: U82(X1,active(X2)) -> U82(X1,X2) 143: U91(mark(X1),X2) -> U91(X1,X2) 144: U91(X1,mark(X2)) -> U91(X1,X2) 145: U91(active(X1),X2) -> U91(X1,X2) 146: U91(X1,active(X2)) -> U91(X1,X2) 147: and(mark(X1),X2) -> and(X1,X2) 148: and(X1,mark(X2)) -> and(X1,X2) 149: and(active(X1),X2) -> and(X1,X2) 150: and(X1,active(X2)) -> and(X1,X2) 151: isNatural(mark(X)) -> isNatural(X) 152: isNatural(active(X)) -> isNatural(X) 153: isLNat(mark(X)) -> isLNat(X) 154: isLNat(active(X)) -> isLNat(X) 155: isPLNat(mark(X)) -> isPLNat(X) 156: isPLNat(active(X)) -> isPLNat(X) 157: tail(mark(X)) -> tail(X) 158: tail(active(X)) -> tail(X) 159: take(mark(X1),X2) -> take(X1,X2) 160: take(X1,mark(X2)) -> take(X1,X2) 161: take(active(X1),X2) -> take(X1,X2) 162: take(X1,active(X2)) -> take(X1,X2) 163: sel(mark(X1),X2) -> sel(X1,X2) 164: sel(X1,mark(X2)) -> sel(X1,X2) 165: sel(active(X1),X2) -> sel(X1,X2) 166: sel(X1,active(X2)) -> sel(X1,X2) Number of strict rules: 166 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #active(U11(tt(),N,XS)) -> #mark(snd(splitAt(N,XS))) #2: #active(U11(tt(),N,XS)) -> #snd(splitAt(N,XS)) #3: #active(U11(tt(),N,XS)) -> #splitAt(N,XS) #4: #snd(active(X)) -> #snd(X) #5: #mark(U21(X1,X2)) -> #active(U21(mark(X1),X2)) #6: #mark(U21(X1,X2)) -> #U21(mark(X1),X2) #7: #mark(U21(X1,X2)) -> #mark(X1) #8: #active(isPLNat(splitAt(V1,V2))) -> #mark(and(isNatural(V1),isLNat(V2))) #9: #active(isPLNat(splitAt(V1,V2))) -> #and(isNatural(V1),isLNat(V2)) #10: #active(isPLNat(splitAt(V1,V2))) -> #isNatural(V1) #11: #active(isPLNat(splitAt(V1,V2))) -> #isLNat(V2) #12: #active(tail(cons(N,XS))) -> #mark(U91(and(isNatural(N),isLNat(XS)),XS)) #13: #active(tail(cons(N,XS))) -> #U91(and(isNatural(N),isLNat(XS)),XS) #14: #active(tail(cons(N,XS))) -> #and(isNatural(N),isLNat(XS)) #15: #active(tail(cons(N,XS))) -> #isNatural(N) #16: #active(tail(cons(N,XS))) -> #isLNat(XS) #17: #U11(X1,active(X2),X3) -> #U11(X1,X2,X3) #18: #mark(sel(X1,X2)) -> #active(sel(mark(X1),mark(X2))) #19: #mark(sel(X1,X2)) -> #sel(mark(X1),mark(X2)) #20: #mark(sel(X1,X2)) -> #mark(X1) #21: #mark(sel(X1,X2)) -> #mark(X2) #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: #mark(snd(X)) -> #active(snd(mark(X))) #26: #mark(snd(X)) -> #snd(mark(X)) #27: #mark(snd(X)) -> #mark(X) #28: #afterNth(mark(X1),X2) -> #afterNth(X1,X2) #29: #and(active(X1),X2) -> #and(X1,X2) #30: #U41(mark(X1),X2) -> #U41(X1,X2) #31: #mark(U11(X1,X2,X3)) -> #active(U11(mark(X1),X2,X3)) #32: #mark(U11(X1,X2,X3)) -> #U11(mark(X1),X2,X3) #33: #mark(U11(X1,X2,X3)) -> #mark(X1) #34: #mark(U101(X1,X2,X3)) -> #active(U101(mark(X1),X2,X3)) #35: #mark(U101(X1,X2,X3)) -> #U101(mark(X1),X2,X3) #36: #mark(U101(X1,X2,X3)) -> #mark(X1) #37: #head(active(X)) -> #head(X) #38: #cons(mark(X1),X2) -> #cons(X1,X2) #39: #sel(mark(X1),X2) -> #sel(X1,X2) #40: #U41(active(X1),X2) -> #U41(X1,X2) #41: #U31(mark(X1),X2) -> #U31(X1,X2) #42: #fst(mark(X)) -> #fst(X) #43: #mark(natsFrom(X)) -> #active(natsFrom(mark(X))) #44: #mark(natsFrom(X)) -> #natsFrom(mark(X)) #45: #mark(natsFrom(X)) -> #mark(X) #46: #mark(U71(X1,X2)) -> #active(U71(mark(X1),X2)) #47: #mark(U71(X1,X2)) -> #U71(mark(X1),X2) #48: #mark(U71(X1,X2)) -> #mark(X1) #49: #U101(X1,active(X2),X3) -> #U101(X1,X2,X3) #50: #and(mark(X1),X2) -> #and(X1,X2) #51: #U82(mark(X1),X2) -> #U82(X1,X2) #52: #mark(s(X)) -> #active(s(mark(X))) #53: #mark(s(X)) -> #s(mark(X)) #54: #mark(s(X)) -> #mark(X) #55: #U71(mark(X1),X2) -> #U71(X1,X2) #56: #splitAt(mark(X1),X2) -> #splitAt(X1,X2) #57: #U51(X1,X2,active(X3)) -> #U51(X1,X2,X3) #58: #fst(active(X)) -> #fst(X) #59: #mark(U91(X1,X2)) -> #active(U91(mark(X1),X2)) #60: #mark(U91(X1,X2)) -> #U91(mark(X1),X2) #61: #mark(U91(X1,X2)) -> #mark(X1) #62: #U81(X1,X2,X3,active(X4)) -> #U81(X1,X2,X3,X4) #63: #head(mark(X)) -> #head(X) #64: #tail(active(X)) -> #tail(X) #65: #mark(isLNat(X)) -> #active(isLNat(X)) #66: #mark(tt()) -> #active(tt()) #67: #isNatural(mark(X)) -> #isNatural(X) #68: #isLNat(active(X)) -> #isLNat(X) #69: #afterNth(X1,mark(X2)) -> #afterNth(X1,X2) #70: #isPLNat(mark(X)) -> #isPLNat(X) #71: #active(U51(tt(),N,XS)) -> #mark(head(afterNth(N,XS))) #72: #active(U51(tt(),N,XS)) -> #head(afterNth(N,XS)) #73: #active(U51(tt(),N,XS)) -> #afterNth(N,XS) #74: #sel(active(X1),X2) -> #sel(X1,X2) #75: #mark(and(X1,X2)) -> #active(and(mark(X1),X2)) #76: #mark(and(X1,X2)) -> #and(mark(X1),X2) #77: #mark(and(X1,X2)) -> #mark(X1) #78: #U51(active(X1),X2,X3) -> #U51(X1,X2,X3) #79: #U81(X1,mark(X2),X3,X4) -> #U81(X1,X2,X3,X4) #80: #mark(nil()) -> #active(nil()) #81: #U101(mark(X1),X2,X3) -> #U101(X1,X2,X3) #82: #mark(splitAt(X1,X2)) -> #active(splitAt(mark(X1),mark(X2))) #83: #mark(splitAt(X1,X2)) -> #splitAt(mark(X1),mark(X2)) #84: #mark(splitAt(X1,X2)) -> #mark(X1) #85: #mark(splitAt(X1,X2)) -> #mark(X2) #86: #U21(X1,active(X2)) -> #U21(X1,X2) #87: #U91(X1,active(X2)) -> #U91(X1,X2) #88: #U51(mark(X1),X2,X3) -> #U51(X1,X2,X3) #89: #mark(afterNth(X1,X2)) -> #active(afterNth(mark(X1),mark(X2))) #90: #mark(afterNth(X1,X2)) -> #afterNth(mark(X1),mark(X2)) #91: #mark(afterNth(X1,X2)) -> #mark(X1) #92: #mark(afterNth(X1,X2)) -> #mark(X2) #93: #active(and(tt(),X)) -> #mark(X) #94: #active(U81(tt(),N,X,XS)) -> #mark(U82(splitAt(N,XS),X)) #95: #active(U81(tt(),N,X,XS)) -> #U82(splitAt(N,XS),X) #96: #active(U81(tt(),N,X,XS)) -> #splitAt(N,XS) #97: #active(U91(tt(),XS)) -> #mark(XS) #98: #U41(X1,active(X2)) -> #U41(X1,X2) #99: #isPLNat(active(X)) -> #isPLNat(X) #100: #mark(U82(X1,X2)) -> #active(U82(mark(X1),X2)) #101: #mark(U82(X1,X2)) -> #U82(mark(X1),X2) #102: #mark(U82(X1,X2)) -> #mark(X1) #103: #splitAt(X1,mark(X2)) -> #splitAt(X1,X2) #104: #U51(X1,X2,mark(X3)) -> #U51(X1,X2,X3) #105: #U31(X1,active(X2)) -> #U31(X1,X2) #106: #active(isNatural(0())) -> #mark(tt()) #107: #U81(X1,X2,X3,mark(X4)) -> #U81(X1,X2,X3,X4) #108: #U101(active(X1),X2,X3) -> #U101(X1,X2,X3) #109: #active(isLNat(take(V1,V2))) -> #mark(and(isNatural(V1),isLNat(V2))) #110: #active(isLNat(take(V1,V2))) -> #and(isNatural(V1),isLNat(V2)) #111: #active(isLNat(take(V1,V2))) -> #isNatural(V1) #112: #active(isLNat(take(V1,V2))) -> #isLNat(V2) #113: #pair(X1,mark(X2)) -> #pair(X1,X2) #114: #U11(X1,X2,mark(X3)) -> #U11(X1,X2,X3) #115: #afterNth(X1,active(X2)) -> #afterNth(X1,X2) #116: #splitAt(X1,active(X2)) -> #splitAt(X1,X2) #117: #mark(U41(X1,X2)) -> #active(U41(mark(X1),X2)) #118: #mark(U41(X1,X2)) -> #U41(mark(X1),X2) #119: #mark(U41(X1,X2)) -> #mark(X1) #120: #U41(X1,mark(X2)) -> #U41(X1,X2) #121: #U101(X1,X2,mark(X3)) -> #U101(X1,X2,X3) #122: #cons(active(X1),X2) -> #cons(X1,X2) #123: #active(afterNth(N,XS)) -> #mark(U11(and(isNatural(N),isLNat(XS)),N,XS)) #124: #active(afterNth(N,XS)) -> #U11(and(isNatural(N),isLNat(XS)),N,XS) #125: #active(afterNth(N,XS)) -> #and(isNatural(N),isLNat(XS)) #126: #active(afterNth(N,XS)) -> #isNatural(N) #127: #active(afterNth(N,XS)) -> #isLNat(XS) #128: #active(sel(N,XS)) -> #mark(U51(and(isNatural(N),isLNat(XS)),N,XS)) #129: #active(sel(N,XS)) -> #U51(and(isNatural(N),isLNat(XS)),N,XS) #130: #active(sel(N,XS)) -> #and(isNatural(N),isLNat(XS)) #131: #active(sel(N,XS)) -> #isNatural(N) #132: #active(sel(N,XS)) -> #isLNat(XS) #133: #sel(X1,mark(X2)) -> #sel(X1,X2) #134: #U11(mark(X1),X2,X3) -> #U11(X1,X2,X3) #135: #mark(U81(X1,X2,X3,X4)) -> #active(U81(mark(X1),X2,X3,X4)) #136: #mark(U81(X1,X2,X3,X4)) -> #U81(mark(X1),X2,X3,X4) #137: #mark(U81(X1,X2,X3,X4)) -> #mark(X1) #138: #U21(active(X1),X2) -> #U21(X1,X2) #139: #U81(X1,X2,mark(X3),X4) -> #U81(X1,X2,X3,X4) #140: #U11(active(X1),X2,X3) -> #U11(X1,X2,X3) #141: #U51(X1,active(X2),X3) -> #U51(X1,X2,X3) #142: #active(fst(pair(X,Y))) -> #mark(U21(and(isLNat(X),isLNat(Y)),X)) #143: #active(fst(pair(X,Y))) -> #U21(and(isLNat(X),isLNat(Y)),X) #144: #active(fst(pair(X,Y))) -> #and(isLNat(X),isLNat(Y)) #145: #active(fst(pair(X,Y))) -> #isLNat(X) #146: #active(fst(pair(X,Y))) -> #isLNat(Y) #147: #s(active(X)) -> #s(X) #148: #mark(isPLNat(X)) -> #active(isPLNat(X)) #149: #active(natsFrom(N)) -> #mark(U41(isNatural(N),N)) #150: #active(natsFrom(N)) -> #U41(isNatural(N),N) #151: #active(natsFrom(N)) -> #isNatural(N) #152: #mark(U61(X1,X2)) -> #active(U61(mark(X1),X2)) #153: #mark(U61(X1,X2)) -> #U61(mark(X1),X2) #154: #mark(U61(X1,X2)) -> #mark(X1) #155: #mark(U51(X1,X2,X3)) -> #active(U51(mark(X1),X2,X3)) #156: #mark(U51(X1,X2,X3)) -> #U51(mark(X1),X2,X3) #157: #mark(U51(X1,X2,X3)) -> #mark(X1) #158: #active(isNatural(head(V1))) -> #mark(isLNat(V1)) #159: #active(isNatural(head(V1))) -> #isLNat(V1) #160: #pair(X1,active(X2)) -> #pair(X1,X2) #161: #sel(X1,active(X2)) -> #sel(X1,X2) #162: #U51(X1,mark(X2),X3) -> #U51(X1,X2,X3) #163: #pair(active(X1),X2) -> #pair(X1,X2) #164: #active(isLNat(natsFrom(V1))) -> #mark(isNatural(V1)) #165: #active(isLNat(natsFrom(V1))) -> #isNatural(V1) #166: #U71(X1,active(X2)) -> #U71(X1,X2) #167: #U21(X1,mark(X2)) -> #U21(X1,X2) #168: #active(U61(tt(),Y)) -> #mark(Y) #169: #mark(fst(X)) -> #active(fst(mark(X))) #170: #mark(fst(X)) -> #fst(mark(X)) #171: #mark(fst(X)) -> #mark(X) #172: #isLNat(mark(X)) -> #isLNat(X) #173: #U81(X1,active(X2),X3,X4) -> #U81(X1,X2,X3,X4) #174: #active(U82(pair(YS,ZS),X)) -> #mark(pair(cons(X,YS),ZS)) #175: #active(U82(pair(YS,ZS),X)) -> #pair(cons(X,YS),ZS) #176: #active(U82(pair(YS,ZS),X)) -> #cons(X,YS) #177: #U31(X1,mark(X2)) -> #U31(X1,X2) #178: #U61(mark(X1),X2) -> #U61(X1,X2) #179: #U31(active(X1),X2) -> #U31(X1,X2) #180: #mark(take(X1,X2)) -> #active(take(mark(X1),mark(X2))) #181: #mark(take(X1,X2)) -> #take(mark(X1),mark(X2)) #182: #mark(take(X1,X2)) -> #mark(X1) #183: #mark(take(X1,X2)) -> #mark(X2) #184: #active(splitAt(0(),XS)) -> #mark(U71(isLNat(XS),XS)) #185: #active(splitAt(0(),XS)) -> #U71(isLNat(XS),XS) #186: #active(splitAt(0(),XS)) -> #isLNat(XS) #187: #U101(X1,X2,active(X3)) -> #U101(X1,X2,X3) #188: #take(X1,active(X2)) -> #take(X1,X2) #189: #U61(X1,mark(X2)) -> #U61(X1,X2) #190: #active(U41(tt(),N)) -> #mark(cons(N,natsFrom(s(N)))) #191: #active(U41(tt(),N)) -> #cons(N,natsFrom(s(N))) #192: #active(U41(tt(),N)) -> #natsFrom(s(N)) #193: #active(U41(tt(),N)) -> #s(N) #194: #mark(U31(X1,X2)) -> #active(U31(mark(X1),X2)) #195: #mark(U31(X1,X2)) -> #U31(mark(X1),X2) #196: #mark(U31(X1,X2)) -> #mark(X1) #197: #mark(0()) -> #active(0()) #198: #and(X1,mark(X2)) -> #and(X1,X2) #199: #active(isPLNat(pair(V1,V2))) -> #mark(and(isLNat(V1),isLNat(V2))) #200: #active(isPLNat(pair(V1,V2))) -> #and(isLNat(V1),isLNat(V2)) #201: #active(isPLNat(pair(V1,V2))) -> #isLNat(V1) #202: #active(isPLNat(pair(V1,V2))) -> #isLNat(V2) #203: #active(isLNat(tail(V1))) -> #mark(isLNat(V1)) #204: #active(isLNat(tail(V1))) -> #isLNat(V1) #205: #pair(mark(X1),X2) -> #pair(X1,X2) #206: #active(splitAt(s(N),cons(X,XS))) -> #mark(U81(and(isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS)) #207: #active(splitAt(s(N),cons(X,XS))) -> #U81(and(isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS) #208: #active(splitAt(s(N),cons(X,XS))) -> #and(isNatural(N),and(isNatural(X),isLNat(XS))) #209: #active(splitAt(s(N),cons(X,XS))) -> #isNatural(N) #210: #active(splitAt(s(N),cons(X,XS))) -> #and(isNatural(X),isLNat(XS)) #211: #active(splitAt(s(N),cons(X,XS))) -> #isNatural(X) #212: #active(splitAt(s(N),cons(X,XS))) -> #isLNat(XS) #213: #U11(X1,X2,active(X3)) -> #U11(X1,X2,X3) #214: #U21(mark(X1),X2) -> #U21(X1,X2) #215: #tail(mark(X)) -> #tail(X) #216: #active(isNatural(sel(V1,V2))) -> #mark(and(isNatural(V1),isLNat(V2))) #217: #active(isNatural(sel(V1,V2))) -> #and(isNatural(V1),isLNat(V2)) #218: #active(isNatural(sel(V1,V2))) -> #isNatural(V1) #219: #active(isNatural(sel(V1,V2))) -> #isLNat(V2) #220: #U81(X1,X2,active(X3),X4) -> #U81(X1,X2,X3,X4) #221: #U91(X1,mark(X2)) -> #U91(X1,X2) #222: #U82(X1,active(X2)) -> #U82(X1,X2) #223: #take(active(X1),X2) -> #take(X1,X2) #224: #and(X1,active(X2)) -> #and(X1,X2) #225: #mark(isNatural(X)) -> #active(isNatural(X)) #226: #afterNth(active(X1),X2) -> #afterNth(X1,X2) #227: #active(isLNat(afterNth(V1,V2))) -> #mark(and(isNatural(V1),isLNat(V2))) #228: #active(isLNat(afterNth(V1,V2))) -> #and(isNatural(V1),isLNat(V2)) #229: #active(isLNat(afterNth(V1,V2))) -> #isNatural(V1) #230: #active(isLNat(afterNth(V1,V2))) -> #isLNat(V2) #231: #active(snd(pair(X,Y))) -> #mark(U61(and(isLNat(X),isLNat(Y)),Y)) #232: #active(snd(pair(X,Y))) -> #U61(and(isLNat(X),isLNat(Y)),Y) #233: #active(snd(pair(X,Y))) -> #and(isLNat(X),isLNat(Y)) #234: #active(snd(pair(X,Y))) -> #isLNat(X) #235: #active(snd(pair(X,Y))) -> #isLNat(Y) #236: #active(isLNat(fst(V1))) -> #mark(isPLNat(V1)) #237: #active(isLNat(fst(V1))) -> #isPLNat(V1) #238: #U91(mark(X1),X2) -> #U91(X1,X2) #239: #U71(active(X1),X2) -> #U71(X1,X2) #240: #mark(tail(X)) -> #active(tail(mark(X))) #241: #mark(tail(X)) -> #tail(mark(X)) #242: #mark(tail(X)) -> #mark(X) #243: #U81(active(X1),X2,X3,X4) -> #U81(X1,X2,X3,X4) #244: #s(mark(X)) -> #s(X) #245: #active(isNatural(s(V1))) -> #mark(isNatural(V1)) #246: #active(isNatural(s(V1))) -> #isNatural(V1) #247: #cons(X1,mark(X2)) -> #cons(X1,X2) #248: #snd(mark(X)) -> #snd(X) #249: #U61(X1,active(X2)) -> #U61(X1,X2) #250: #U101(X1,mark(X2),X3) -> #U101(X1,X2,X3) #251: #U81(mark(X1),X2,X3,X4) -> #U81(X1,X2,X3,X4) #252: #active(take(N,XS)) -> #mark(U101(and(isNatural(N),isLNat(XS)),N,XS)) #253: #active(take(N,XS)) -> #U101(and(isNatural(N),isLNat(XS)),N,XS) #254: #active(take(N,XS)) -> #and(isNatural(N),isLNat(XS)) #255: #active(take(N,XS)) -> #isNatural(N) #256: #active(take(N,XS)) -> #isLNat(XS) #257: #active(isLNat(snd(V1))) -> #mark(isPLNat(V1)) #258: #active(isLNat(snd(V1))) -> #isPLNat(V1) #259: #active(isLNat(nil())) -> #mark(tt()) #260: #active(U21(tt(),X)) -> #mark(X) #261: #take(mark(X1),X2) -> #take(X1,X2) #262: #splitAt(active(X1),X2) -> #splitAt(X1,X2) #263: #active(U101(tt(),N,XS)) -> #mark(fst(splitAt(N,XS))) #264: #active(U101(tt(),N,XS)) -> #fst(splitAt(N,XS)) #265: #active(U101(tt(),N,XS)) -> #splitAt(N,XS) #266: #U82(X1,mark(X2)) -> #U82(X1,X2) #267: #U71(X1,mark(X2)) -> #U71(X1,X2) #268: #mark(pair(X1,X2)) -> #active(pair(mark(X1),mark(X2))) #269: #mark(pair(X1,X2)) -> #pair(mark(X1),mark(X2)) #270: #mark(pair(X1,X2)) -> #mark(X1) #271: #mark(pair(X1,X2)) -> #mark(X2) #272: #take(X1,mark(X2)) -> #take(X1,X2) #273: #active(U71(tt(),XS)) -> #mark(pair(nil(),XS)) #274: #active(U71(tt(),XS)) -> #pair(nil(),XS) #275: #isNatural(active(X)) -> #isNatural(X) #276: #U82(active(X1),X2) -> #U82(X1,X2) #277: #U61(active(X1),X2) -> #U61(X1,X2) #278: #active(head(cons(N,XS))) -> #mark(U31(and(isNatural(N),isLNat(XS)),N)) #279: #active(head(cons(N,XS))) -> #U31(and(isNatural(N),isLNat(XS)),N) #280: #active(head(cons(N,XS))) -> #and(isNatural(N),isLNat(XS)) #281: #active(head(cons(N,XS))) -> #isNatural(N) #282: #active(head(cons(N,XS))) -> #isLNat(XS) #283: #U91(active(X1),X2) -> #U91(X1,X2) #284: #cons(X1,active(X2)) -> #cons(X1,X2) #285: #natsFrom(mark(X)) -> #natsFrom(X) #286: #active(U31(tt(),N)) -> #mark(N) #287: #natsFrom(active(X)) -> #natsFrom(X) #288: #U11(X1,mark(X2),X3) -> #U11(X1,X2,X3) #289: #mark(head(X)) -> #active(head(mark(X))) #290: #mark(head(X)) -> #head(mark(X)) #291: #mark(head(X)) -> #mark(X) #292: #active(isLNat(cons(V1,V2))) -> #mark(and(isNatural(V1),isLNat(V2))) #293: #active(isLNat(cons(V1,V2))) -> #and(isNatural(V1),isLNat(V2)) #294: #active(isLNat(cons(V1,V2))) -> #isNatural(V1) #295: #active(isLNat(cons(V1,V2))) -> #isLNat(V2) Number of SCCs: 28, DPs: 187, edges: 2319 SCC { #67 #275 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: x1 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #67 #275 Number of SCCs: 27, DPs: 185, edges: 2315 SCC { #37 #63 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: x1 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #37 #63 Number of SCCs: 26, DPs: 183, edges: 2311 SCC { #68 #172 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: x1 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #68 #172 Number of SCCs: 25, DPs: 181, edges: 2307 SCC { #64 #215 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: x1 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #64 #215 Number of SCCs: 24, DPs: 179, edges: 2303 SCC { #42 #58 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: x1 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #42 #58 Number of SCCs: 23, DPs: 177, edges: 2299 SCC { #147 #244 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: x1 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #147 #244 Number of SCCs: 22, DPs: 175, edges: 2295 SCC { #70 #99 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: x1 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #70 #99 Number of SCCs: 21, DPs: 173, edges: 2291 SCC { #285 #287 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: x1 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #285 #287 Number of SCCs: 20, DPs: 171, edges: 2287 SCC { #4 #248 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: x1 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #4 #248 Number of SCCs: 19, DPs: 169, edges: 2283 SCC { #30 #40 #98 #120 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: x2 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #98 #120 Number of SCCs: 19, DPs: 167, edges: 2271 SCC { #30 #40 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: x1 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #30 #40 Number of SCCs: 18, DPs: 165, edges: 2267 SCC { #41 #105 #177 #179 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: x1 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #41 #179 Number of SCCs: 19, DPs: 163, edges: 2255 SCC { #105 #177 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: x2 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #105 #177 Number of SCCs: 18, DPs: 161, edges: 2251 SCC { #113 #160 #163 #205 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: x2 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #113 #160 Number of SCCs: 19, DPs: 159, edges: 2239 SCC { #163 #205 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: x1 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #163 #205 Number of SCCs: 18, DPs: 157, edges: 2235 SCC { #87 #221 #238 #283 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: x2 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #87 #221 Number of SCCs: 19, DPs: 155, edges: 2223 SCC { #238 #283 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: x1 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #238 #283 Number of SCCs: 18, DPs: 153, edges: 2219 SCC { #188 #223 #261 #272 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: x2 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #188 #272 Number of SCCs: 19, DPs: 151, edges: 2207 SCC { #223 #261 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: x1 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #223 #261 Number of SCCs: 18, DPs: 149, edges: 2203 SCC { #86 #138 #167 #214 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: x1 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #138 #214 Number of SCCs: 19, DPs: 147, edges: 2191 SCC { #86 #167 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: x2 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #86 #167 Number of SCCs: 18, DPs: 145, edges: 2187 SCC { #28 #69 #115 #226 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: x1 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #28 #226 Number of SCCs: 19, DPs: 143, edges: 2175 SCC { #69 #115 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: x2 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #69 #115 Number of SCCs: 18, DPs: 141, edges: 2171 SCC { #178 #189 #249 #277 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: x2 Usable rules: { } Removed DPs: #189 #249 Number of SCCs: 19, DPs: 139, edges: 2159 SCC { #178 #277 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: x1 Usable rules: { } Removed DPs: #178 #277 Number of SCCs: 18, DPs: 137, edges: 2155 SCC { #29 #50 #198 #224 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: x2 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #198 #224 Number of SCCs: 19, DPs: 135, edges: 2143 SCC { #29 #50 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: x1 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #29 #50 Number of SCCs: 18, DPs: 133, edges: 2139 SCC { #56 #103 #116 #262 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: x1 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #56 #262 Number of SCCs: 19, DPs: 131, edges: 2127 SCC { #103 #116 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: x2 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #103 #116 Number of SCCs: 18, DPs: 129, edges: 2123 SCC { #51 #222 #266 #276 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: x2 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #222 #266 Number of SCCs: 19, DPs: 127, edges: 2111 SCC { #51 #276 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: x1 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #51 #276 Number of SCCs: 18, DPs: 125, edges: 2107 SCC { #38 #122 #247 #284 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: x2 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #247 #284 Number of SCCs: 19, DPs: 123, edges: 2095 SCC { #38 #122 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: x1 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #38 #122 Number of SCCs: 18, DPs: 121, edges: 2091 SCC { #55 #166 #239 #267 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: x1 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #55 #239 Number of SCCs: 19, DPs: 119, edges: 2079 SCC { #166 #267 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: x2 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #166 #267 Number of SCCs: 18, DPs: 117, edges: 2075 SCC { #39 #74 #133 #161 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: x2 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #133 #161 Number of SCCs: 19, DPs: 115, edges: 2063 SCC { #39 #74 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: x1 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #39 #74 Number of SCCs: 18, DPs: 113, edges: 2059 SCC { #49 #81 #108 #121 #187 #250 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: x2 + x3 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #49 #121 #187 #250 Number of SCCs: 19, DPs: 109, edges: 2027 SCC { #81 #108 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: x1 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #81 #108 Number of SCCs: 18, DPs: 107, edges: 2023 SCC { #57 #78 #88 #104 #141 #162 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: x1 + x2 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #78 #88 #141 #162 Number of SCCs: 19, DPs: 103, edges: 1991 SCC { #57 #104 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: x3 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #57 #104 Number of SCCs: 18, DPs: 101, edges: 1987 SCC { #17 #114 #134 #140 #213 #288 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: x1 + x2 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #17 #134 #140 #288 Number of SCCs: 19, DPs: 97, edges: 1955 SCC { #114 #213 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: x3 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #114 #213 Number of SCCs: 18, DPs: 95, edges: 1951 SCC { #62 #79 #107 #139 #173 #220 #243 #251 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: x1 + x3 + x4 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #62 #107 #139 #220 #243 #251 Number of SCCs: 19, DPs: 89, edges: 1891 SCC { #79 #173 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: 0 #U81(x1,x2,x3,x4) weight: x2 and(x1,x2) weight: 0 U101(x1,x2,x3) weight: 0 pair(x1,x2) weight: 0 fst(x1) weight: 0 natsFrom(x1) weight: 0 #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: 0 tail(x1) weight: 0 #mark(x1) weight: 0 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: 0 #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: 0 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: 0 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1,x2) weight: 0 head(x1) weight: 0 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #natsFrom(x1) weight: 0 #active(x1) weight: 0 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: 0 U82(x1,x2) weight: 0 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: 0 #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { } Removed DPs: #79 #173 Number of SCCs: 18, DPs: 87, edges: 1887 SCC { #1 #5 #7 #8 #12 #18 #20 #21 #24 #25 #27 #31 #33 #34 #36 #43 #45 #46 #48 #54 #59 #61 #65 #71 #75 #77 #82 #84 #85 #89 #91..94 #97 #100 #102 #109 #117 #119 #123 #128 #135 #137 #142 #148 #149 #152 #154 #155 #157 #158 #164 #168 #169 #171 #174 #180 #182..184 #190 #194 #196 #199 #203 #206 #216 #225 #227 #231 #236 #240 #242 #245 #252 #257 #260 #263 #270 #271 #273 #278 #286 #289 #291 #292 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. U21(x1,x2) weight: max{(/ 1 64) + x2, (/ 1 32) + x1} U11(x1,x2,x3) weight: max{(/ 19 64) + x3, (/ 5 16) + x2, (/ 7 32) + x1} #cons(x1,x2) weight: 0 s(x1) weight: x1 #take(x1,x2) weight: 0 isPLNat(x1) weight: (/ 1 16) + x1 U91(x1,x2) weight: max{(/ 1 32) + x2, (/ 1 64) + x1} #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: max{(/ 3 8) + x2, (/ 23 64) + x1} U71(x1,x2) weight: max{(/ 11 64) + x2, (/ 3 64) + x1} #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: max{x2, (/ 3 64) + x1} U101(x1,x2,x3) weight: max{(/ 21 64) + x3, (/ 11 32) + x2, (/ 11 64) + x1} pair(x1,x2) weight: max{(/ 1 64) + x2, (/ 3 64) + x1} fst(x1) weight: (/ 3 32) + x1 natsFrom(x1) weight: (/ 5 64) + x1 #head(x1) weight: 0 splitAt(x1,x2) weight: max{(/ 3 16) + x2, (/ 7 32) + x1} #fst(x1) weight: 0 isNatural(x1) weight: (/ 3 64) + x1 tail(x1) weight: (/ 1 8) + x1 #mark(x1) weight: x1 0() weight: (/ 5 64) #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: max{(/ 5 8) + x2, (/ 41 64) + x1} #s(x1) weight: 0 afterNth(x1,x2) weight: max{(/ 21 64) + x2, (/ 11 32) + x1} #isPLNat(x1) weight: 0 nil() weight: (/ 7 64) isLNat(x1) weight: (/ 1 64) + x1 #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 32) + x1} #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: x1 U31(x1,x2) weight: max{(/ 1 64) + x2, (/ 1 32) + x1} head(x1) weight: (/ 9 64) + x1 #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: max{x2, (/ 5 64) + x1} #natsFrom(x1) weight: 0 #active(x1) weight: x1 snd(x1) weight: (/ 1 16) + x1 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: max{(/ 3 16) + x4, (/ 1 8) + x3, (/ 7 32) + x2, (/ 7 64) + x1} U82(x1,x2) weight: max{(/ 1 8) + x2, x1} tt() weight: (/ 1 8) #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: max{(/ 1 2) + x3, (/ 39 64) + x2, (/ 33 64) + x1} U41(x1,x2) weight: max{(/ 5 64) + x2, (/ 1 64) + x1} #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { 1..166 } Removed DPs: #1 #7 #8 #12 #20 #21 #24 #27 #33 #36 #45 #48 #61 #71 #77 #84 #85 #91 #92 #97 #109 #119 #123 #128 #137 #142 #154 #157 #158 #164 #168 #171 #182..184 #196 #199 #203 #216 #227 #231 #236 #242 #252 #257 #260 #263 #270 #271 #273 #278 #286 #291 Number of SCCs: 20, DPs: 12, edges: 27 SCC { #225 #245 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: 0 U11(x1,x2,x3) weight: x2 #cons(x1,x2) weight: 0 s(x1) weight: (/ 1 2) + x1 #take(x1,x2) weight: 0 isPLNat(x1) weight: 0 U91(x1,x2) weight: 0 #U101(x1,x2,x3) weight: 0 #U82(x1,x2) weight: 0 take(x1,x2) weight: 0 U71(x1,x2) weight: x2 #U81(x1,x2,x3,x4) weight: 0 and(x1,x2) weight: (/ 1 4) U101(x1,x2,x3) weight: x2 pair(x1,x2) weight: (/ 1 4) + x2 fst(x1) weight: 0 natsFrom(x1) weight: (/ 1 4) #head(x1) weight: 0 splitAt(x1,x2) weight: 0 #fst(x1) weight: 0 isNatural(x1) weight: (/ 1 4) + x1 tail(x1) weight: 0 #mark(x1) weight: (/ 1 4) + x1 0() weight: 0 #sel(x1,x2) weight: 0 #isLNat(x1) weight: 0 sel(x1,x2) weight: 0 #s(x1) weight: 0 afterNth(x1,x2) weight: (/ 1 4) #isPLNat(x1) weight: 0 nil() weight: 0 isLNat(x1) weight: (/ 1 4) #tail(x1) weight: 0 #splitAt(x1,x2) weight: 0 mark(x1) weight: (/ 1 4) + x1 #afterNth(x1,x2) weight: 0 U61(x1,x2) weight: x2 #U51(x1,x2,x3) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 4) + x1 U31(x1,x2) weight: x2 head(x1) weight: (/ 1 4) #snd(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: (/ 1 4) #natsFrom(x1) weight: 0 #active(x1) weight: x1 snd(x1) weight: 0 #U21(x1,x2) weight: 0 U81(x1,x2,x3,x4) weight: x2 + x3 U82(x1,x2) weight: x2 tt() weight: 0 #U71(x1,x2) weight: 0 #isNatural(x1) weight: 0 #pair(x1,x2) weight: 0 U51(x1,x2,x3) weight: 0 U41(x1,x2) weight: (/ 1 4) #U31(x1,x2) weight: 0 #and(x1,x2) weight: 0 #U91(x1,x2) weight: 0 #U61(x1,x2) weight: 0 Usable rules: { 151 152 } Removed DPs: #225 #245 Number of SCCs: 19, DPs: 10, edges: 25 SCC { #54 #65 #75 #82 #93 #94 #102 #135 #206 #292 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded. U21(x1,x2) status: [x2] precedence above: U11(x1,x2,x3) status: [x1] precedence above: U31 #cons(x1,x2) status: [x2] precedence above: s(x1) status: [x1] precedence above: natsFrom mark U31 U41 #take(x1,x2) status: [x2] precedence above: isPLNat(x1) status: [x1] precedence above: and splitAt #mark #active U81 U91(x1,x2) status: [x1,x2] precedence above: mark U31 #U101(x1,x2,x3) status: [x2,x1] precedence above: #U82(x1,x2) status: [x1] precedence above: take(x1,x2) status: [] precedence above: isPLNat and U101 splitAt #mark mark U31 #active snd U81 tt U71(x1,x2) status: [x1] precedence above: mark U31 #U81(x1,x2,x3,x4) status: [x1,x2,x4,x3] precedence above: and(x1,x2) status: [x2] precedence above: isPLNat splitAt #mark #active U81 U101(x1,x2,x3) status: [] precedence above: isPLNat take and splitAt #mark mark U31 #active snd U81 tt pair(x1,x2) status: [x2,x1] precedence above: isPLNat and splitAt #mark isLNat mark U61 U31 #active snd U81 tt fst(x1) status: [] precedence above: natsFrom(x1) status: [x1] precedence above: mark U31 #head(x1) status: [] precedence above: splitAt(x1,x2) status: [] precedence above: U81 #fst(x1) status: [] precedence above: isNatural(x1) status: x1 tail(x1) status: [x1] precedence above: #mark(x1) status: [x1] precedence above: isPLNat and splitAt #active U81 0() status: [] precedence above: U21 isPLNat U91 take and U101 pair fst splitAt #mark afterNth isLNat mark U61 active U31 head #active snd U81 tt #sel(x1,x2) status: [x1] precedence above: #isLNat(x1) status: [] precedence above: sel(x1,x2) status: [] precedence above: #s(x1) status: [] precedence above: afterNth(x1,x2) status: [x2,x1] precedence above: #isPLNat(x1) status: [] precedence above: nil() status: [] precedence above: mark U31 snd tt isLNat(x1) status: [x1] precedence above: isPLNat and pair splitAt #mark mark U61 U31 #active snd U81 tt #tail(x1) status: [] precedence above: #splitAt(x1,x2) status: [x2] precedence above: mark(x1) status: [x1] precedence above: U31 #afterNth(x1,x2) status: [x2] precedence above: U61(x1,x2) status: [x2] precedence above: #U51(x1,x2,x3) status: [x3,x1,x2] precedence above: #U11(x1,x2,x3) status: [x1] precedence above: active(x1) status: [x1] precedence above: U21 isPLNat U91 take and U101 pair fst splitAt #mark 0 afterNth isLNat mark U61 U31 head #active snd U81 tt U31(x1,x2) status: x1 head(x1) status: [x1] precedence above: #snd(x1) status: [] precedence above: #U41(x1,x2) status: [x1,x2] precedence above: cons(x1,x2) status: [x1,x2] precedence above: isPLNat U91 and pair splitAt #mark isLNat mark U61 U31 #active snd U81 U82 tt #natsFrom(x1) status: [] precedence above: #active(x1) status: [x1] precedence above: isPLNat and splitAt #mark U81 snd(x1) status: [] precedence above: #U21(x1,x2) status: [x1] precedence above: U81(x1,x2,x3,x4) status: [] precedence above: splitAt U82(x1,x2) status: x1 tt() status: [] precedence above: mark U31 snd #U71(x1,x2) status: [x2] precedence above: #isNatural(x1) status: [] precedence above: #pair(x1,x2) status: [x2,x1] precedence above: U51(x1,x2,x3) status: [x1,x2,x3] precedence above: afterNth mark U31 head U41(x1,x2) status: [x2,x1] precedence above: s natsFrom mark U31 #U31(x1,x2) status: [x2] precedence above: #and(x1,x2) status: [x1] precedence above: #U91(x1,x2) status: [x2] precedence above: #U61(x1,x2) status: [x1,x2] precedence above: Usable rules: { 75..78 105 106 131..142 147..150 153 154 } Removed DPs: #54 #93 #292 Number of SCCs: 19, DPs: 5, edges: 7 SCC { #82 #94 #102 #135 #206 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. U21(x1,x2) weight: max{0, (/ 1 8) + x2} status: [] precedence above: U11(x1,x2,x3) weight: max{(/ 94559 8) + x3, (/ 94555 8) + x2, (/ 1 8) + x1} status: [x2] precedence above: #cons(x1,x2) weight: x2 status: [] precedence above: s(x1) weight: x1 status: [x1] precedence above: isPLNat U71 pair isNatural afterNth isLNat snd tt #take(x1,x2) weight: (/ 1 8) status: [] precedence above: isPLNat(x1) weight: 0 status: [] precedence above: s U71 pair isNatural afterNth isLNat snd tt U91(x1,x2) weight: max{(/ 188033 8) + x2, (/ 94017 4) + x1} status: [x1] precedence above: #U101(x1,x2,x3) weight: x3 status: [] precedence above: #U82(x1,x2) weight: x2 status: [] precedence above: take(x1,x2) weight: 11820 + x2 + x1 status: [] precedence above: s isPLNat U71 and U101 pair isNatural afterNth isLNat head snd tt U51 U71(x1,x2) weight: max{0, x2} status: [x2] precedence above: s isPLNat pair isNatural afterNth isLNat snd tt #U81(x1,x2,x3,x4) weight: (/ 1 8) + x4 + x3 + x2 + x1 status: [x4,x3,x2,x1] precedence above: and(x1,x2) weight: max{0, x2} status: x2 U101(x1,x2,x3) weight: max{0, (/ 94559 8) + x3, (/ 94555 8) + x2} status: [] precedence above: pair(x1,x2) weight: max{x2, x1} status: [x2] precedence above: s isPLNat U71 isNatural afterNth isLNat snd tt fst(x1) weight: (/ 1 4) + x1 status: [] precedence above: s isPLNat U71 and pair isNatural afterNth isLNat mark U61 active head cons snd tt U51 natsFrom(x1) weight: (/ 1 8) + x1 status: [] precedence above: and cons U41 #head(x1) weight: (/ 1 8) status: [] precedence above: splitAt(x1,x2) weight: max{(/ 23639 2) + x2, x1} status: [x1] precedence above: s isPLNat U71 pair isNatural afterNth isLNat snd U81 U82 tt #fst(x1) weight: (/ 1 8) status: [] precedence above: isNatural(x1) weight: 0 status: [] precedence above: s isPLNat U71 pair afterNth isLNat snd tt tail(x1) weight: (/ 188035 8) + x1 status: [] precedence above: #mark(x1) weight: (/ 23639 2) + x1 status: [x1] precedence above: s isPLNat U71 pair splitAt isNatural afterNth isLNat head #active snd U81 U82 tt U51 0() weight: 0 status: [] precedence above: #sel(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x2,x1] precedence above: #isLNat(x1) weight: (/ 1 8) status: [] precedence above: sel(x1,x2) weight: 11821 + x2 + x1 status: [x1,x2] precedence above: s isPLNat U71 pair isNatural afterNth isLNat head snd tt U51 #s(x1) weight: x1 status: [] precedence above: afterNth(x1,x2) weight: max{11820 + x2, (/ 23641 2) + x1} status: [x1] precedence above: s isPLNat U71 pair isNatural isLNat snd tt #isPLNat(x1) weight: (/ 1 8) status: [] precedence above: nil() weight: 0 status: [] precedence above: isLNat(x1) weight: 0 status: [] precedence above: s isPLNat U71 pair isNatural afterNth snd tt #tail(x1) weight: (/ 1 8) status: [] precedence above: #splitAt(x1,x2) weight: x2 status: [] precedence above: mark(x1) weight: x1 status: x1 #afterNth(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x2,x1] precedence above: U61(x1,x2) weight: max{(/ 1 8) + x2, x1} status: [x1,x2] precedence above: active #U51(x1,x2,x3) weight: (/ 1 8) + x3 + x2 + x1 status: [x3,x2] precedence above: #U11(x1,x2,x3) weight: x3 + x2 status: [x3] precedence above: active(x1) weight: x1 status: x1 U31(x1,x2) weight: max{0, (/ 1 8) + x2} status: [] precedence above: head(x1) weight: (/ 1 4) + x1 status: [] precedence above: s isPLNat U71 pair isNatural afterNth isLNat snd tt U51 #snd(x1) weight: (/ 1 8) status: [] precedence above: #U41(x1,x2) weight: x2 status: [] precedence above: cons(x1,x2) weight: max{x2, x1} status: [] precedence above: and #natsFrom(x1) weight: (/ 1 8) status: [] precedence above: #active(x1) weight: (/ 23639 2) + x1 status: [x1] precedence above: s isPLNat U71 pair splitAt isNatural #mark afterNth isLNat head snd U81 U82 tt U51 snd(x1) weight: (/ 1 4) + x1 status: [x1] precedence above: s isPLNat U71 pair isNatural afterNth isLNat tt #U21(x1,x2) weight: x2 status: [x2] precedence above: U81(x1,x2,x3,x4) weight: max{0, (/ 23639 2) + x4, x3, x2} status: [x2,x4] precedence above: s isPLNat U71 pair splitAt isNatural afterNth isLNat snd U82 tt U82(x1,x2) weight: max{x2, x1} status: [x1] precedence above: s isPLNat U71 pair isNatural afterNth isLNat snd tt tt() weight: 0 status: [] precedence above: #U71(x1,x2) weight: x1 status: [x1] precedence above: #isNatural(x1) weight: x1 status: [] precedence above: #pair(x1,x2) weight: x2 status: [] precedence above: U51(x1,x2,x3) weight: max{(/ 94567 8) + x3, (/ 47283 4) + x2, (/ 94563 8) + x1} status: [x3,x1,x2] precedence above: s isPLNat U71 pair isNatural afterNth isLNat head snd tt U41(x1,x2) weight: max{0, (/ 1 8) + x2} status: [] precedence above: and cons #U31(x1,x2) weight: (/ 1 8) + x2 + x1 status: [] precedence above: #and(x1,x2) weight: (/ 1 8) status: [] precedence above: #U91(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x1,x2] precedence above: #U61(x1,x2) weight: x2 status: [x2] precedence above: Usable rules: { 1..166 } Removed DPs: #102 Number of SCCs: 18, DPs: 0, edges: 0 YES