Input TRS: 1: a__U11(tt(),N,XS) -> a__U12(tt(),N,XS) 2: a__U12(tt(),N,XS) -> a__snd(a__splitAt(mark(N),mark(XS))) 3: a__U21(tt(),X) -> a__U22(tt(),X) 4: a__U22(tt(),X) -> mark(X) 5: a__U31(tt(),N) -> a__U32(tt(),N) 6: a__U32(tt(),N) -> mark(N) 7: a__U41(tt(),N,XS) -> a__U42(tt(),N,XS) 8: a__U42(tt(),N,XS) -> a__head(a__afterNth(mark(N),mark(XS))) 9: a__U51(tt(),Y) -> a__U52(tt(),Y) 10: a__U52(tt(),Y) -> mark(Y) 11: a__U61(tt(),N,X,XS) -> a__U62(tt(),N,X,XS) 12: a__U62(tt(),N,X,XS) -> a__U63(tt(),N,X,XS) 13: a__U63(tt(),N,X,XS) -> a__U64(a__splitAt(mark(N),mark(XS)),X) 14: a__U64(pair(YS,ZS),X) -> pair(cons(mark(X),YS),mark(ZS)) 15: a__U71(tt(),XS) -> a__U72(tt(),XS) 16: a__U72(tt(),XS) -> mark(XS) 17: a__U81(tt(),N,XS) -> a__U82(tt(),N,XS) 18: a__U82(tt(),N,XS) -> a__fst(a__splitAt(mark(N),mark(XS))) 19: a__afterNth(N,XS) -> a__U11(tt(),N,XS) 20: a__fst(pair(X,Y)) -> a__U21(tt(),X) 21: a__head(cons(N,XS)) -> a__U31(tt(),N) 22: a__natsFrom(N) -> cons(mark(N),natsFrom(s(N))) 23: a__sel(N,XS) -> a__U41(tt(),N,XS) 24: a__snd(pair(X,Y)) -> a__U51(tt(),Y) 25: a__splitAt(0(),XS) -> pair(nil(),mark(XS)) 26: a__splitAt(s(N),cons(X,XS)) -> a__U61(tt(),N,X,XS) 27: a__tail(cons(N,XS)) -> a__U71(tt(),XS) 28: a__take(N,XS) -> a__U81(tt(),N,XS) 29: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) 30: mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3) 31: mark(snd(X)) -> a__snd(mark(X)) 32: mark(splitAt(X1,X2)) -> a__splitAt(mark(X1),mark(X2)) 33: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) 34: mark(U22(X1,X2)) -> a__U22(mark(X1),X2) 35: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) 36: mark(U32(X1,X2)) -> a__U32(mark(X1),X2) 37: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) 38: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3) 39: mark(head(X)) -> a__head(mark(X)) 40: mark(afterNth(X1,X2)) -> a__afterNth(mark(X1),mark(X2)) 41: mark(U51(X1,X2)) -> a__U51(mark(X1),X2) 42: mark(U52(X1,X2)) -> a__U52(mark(X1),X2) 43: mark(U61(X1,X2,X3,X4)) -> a__U61(mark(X1),X2,X3,X4) 44: mark(U62(X1,X2,X3,X4)) -> a__U62(mark(X1),X2,X3,X4) 45: mark(U63(X1,X2,X3,X4)) -> a__U63(mark(X1),X2,X3,X4) 46: mark(U64(X1,X2)) -> a__U64(mark(X1),X2) 47: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) 48: mark(U72(X1,X2)) -> a__U72(mark(X1),X2) 49: mark(U81(X1,X2,X3)) -> a__U81(mark(X1),X2,X3) 50: mark(U82(X1,X2,X3)) -> a__U82(mark(X1),X2,X3) 51: mark(fst(X)) -> a__fst(mark(X)) 52: mark(natsFrom(X)) -> a__natsFrom(mark(X)) 53: mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) 54: mark(tail(X)) -> a__tail(mark(X)) 55: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) 56: mark(tt()) -> tt() 57: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2)) 58: mark(cons(X1,X2)) -> cons(mark(X1),X2) 59: mark(s(X)) -> s(mark(X)) 60: mark(0()) -> 0() 61: mark(nil()) -> nil() 62: a__U11(X1,X2,X3) -> U11(X1,X2,X3) 63: a__U12(X1,X2,X3) -> U12(X1,X2,X3) 64: a__snd(X) -> snd(X) 65: a__splitAt(X1,X2) -> splitAt(X1,X2) 66: a__U21(X1,X2) -> U21(X1,X2) 67: a__U22(X1,X2) -> U22(X1,X2) 68: a__U31(X1,X2) -> U31(X1,X2) 69: a__U32(X1,X2) -> U32(X1,X2) 70: a__U41(X1,X2,X3) -> U41(X1,X2,X3) 71: a__U42(X1,X2,X3) -> U42(X1,X2,X3) 72: a__head(X) -> head(X) 73: a__afterNth(X1,X2) -> afterNth(X1,X2) 74: a__U51(X1,X2) -> U51(X1,X2) 75: a__U52(X1,X2) -> U52(X1,X2) 76: a__U61(X1,X2,X3,X4) -> U61(X1,X2,X3,X4) 77: a__U62(X1,X2,X3,X4) -> U62(X1,X2,X3,X4) 78: a__U63(X1,X2,X3,X4) -> U63(X1,X2,X3,X4) 79: a__U64(X1,X2) -> U64(X1,X2) 80: a__U71(X1,X2) -> U71(X1,X2) 81: a__U72(X1,X2) -> U72(X1,X2) 82: a__U81(X1,X2,X3) -> U81(X1,X2,X3) 83: a__U82(X1,X2,X3) -> U82(X1,X2,X3) 84: a__fst(X) -> fst(X) 85: a__natsFrom(X) -> natsFrom(X) 86: a__sel(X1,X2) -> sel(X1,X2) 87: a__tail(X) -> tail(X) 88: a__take(X1,X2) -> take(X1,X2) Number of strict rules: 88 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #a__U12(tt(),N,XS) -> #a__snd(a__splitAt(mark(N),mark(XS))) #2: #a__U12(tt(),N,XS) -> #a__splitAt(mark(N),mark(XS)) #3: #a__U12(tt(),N,XS) -> #mark(N) #4: #a__U12(tt(),N,XS) -> #mark(XS) #5: #mark(U61(X1,X2,X3,X4)) -> #a__U61(mark(X1),X2,X3,X4) #6: #mark(U61(X1,X2,X3,X4)) -> #mark(X1) #7: #mark(U11(X1,X2,X3)) -> #a__U11(mark(X1),X2,X3) #8: #mark(U11(X1,X2,X3)) -> #mark(X1) #9: #mark(U31(X1,X2)) -> #a__U31(mark(X1),X2) #10: #mark(U31(X1,X2)) -> #mark(X1) #11: #mark(U64(X1,X2)) -> #a__U64(mark(X1),X2) #12: #mark(U64(X1,X2)) -> #mark(X1) #13: #mark(U52(X1,X2)) -> #a__U52(mark(X1),X2) #14: #mark(U52(X1,X2)) -> #mark(X1) #15: #mark(U51(X1,X2)) -> #a__U51(mark(X1),X2) #16: #mark(U51(X1,X2)) -> #mark(X1) #17: #mark(U41(X1,X2,X3)) -> #a__U41(mark(X1),X2,X3) #18: #mark(U41(X1,X2,X3)) -> #mark(X1) #19: #mark(U71(X1,X2)) -> #a__U71(mark(X1),X2) #20: #mark(U71(X1,X2)) -> #mark(X1) #21: #mark(sel(X1,X2)) -> #a__sel(mark(X1),mark(X2)) #22: #mark(sel(X1,X2)) -> #mark(X1) #23: #mark(sel(X1,X2)) -> #mark(X2) #24: #mark(U72(X1,X2)) -> #a__U72(mark(X1),X2) #25: #mark(U72(X1,X2)) -> #mark(X1) #26: #mark(cons(X1,X2)) -> #mark(X1) #27: #mark(U42(X1,X2,X3)) -> #a__U42(mark(X1),X2,X3) #28: #mark(U42(X1,X2,X3)) -> #mark(X1) #29: #a__U32(tt(),N) -> #mark(N) #30: #mark(s(X)) -> #mark(X) #31: #mark(take(X1,X2)) -> #a__take(mark(X1),mark(X2)) #32: #mark(take(X1,X2)) -> #mark(X1) #33: #mark(take(X1,X2)) -> #mark(X2) #34: #mark(afterNth(X1,X2)) -> #a__afterNth(mark(X1),mark(X2)) #35: #mark(afterNth(X1,X2)) -> #mark(X1) #36: #mark(afterNth(X1,X2)) -> #mark(X2) #37: #mark(fst(X)) -> #a__fst(mark(X)) #38: #mark(fst(X)) -> #mark(X) #39: #a__U63(tt(),N,X,XS) -> #a__U64(a__splitAt(mark(N),mark(XS)),X) #40: #a__U63(tt(),N,X,XS) -> #a__splitAt(mark(N),mark(XS)) #41: #a__U63(tt(),N,X,XS) -> #mark(N) #42: #a__U63(tt(),N,X,XS) -> #mark(XS) #43: #a__U51(tt(),Y) -> #a__U52(tt(),Y) #44: #a__U61(tt(),N,X,XS) -> #a__U62(tt(),N,X,XS) #45: #mark(pair(X1,X2)) -> #mark(X1) #46: #mark(pair(X1,X2)) -> #mark(X2) #47: #a__snd(pair(X,Y)) -> #a__U51(tt(),Y) #48: #a__sel(N,XS) -> #a__U41(tt(),N,XS) #49: #mark(U63(X1,X2,X3,X4)) -> #a__U63(mark(X1),X2,X3,X4) #50: #mark(U63(X1,X2,X3,X4)) -> #mark(X1) #51: #a__U62(tt(),N,X,XS) -> #a__U63(tt(),N,X,XS) #52: #mark(snd(X)) -> #a__snd(mark(X)) #53: #mark(snd(X)) -> #mark(X) #54: #a__U64(pair(YS,ZS),X) -> #mark(X) #55: #a__U64(pair(YS,ZS),X) -> #mark(ZS) #56: #mark(U12(X1,X2,X3)) -> #a__U12(mark(X1),X2,X3) #57: #mark(U12(X1,X2,X3)) -> #mark(X1) #58: #mark(natsFrom(X)) -> #a__natsFrom(mark(X)) #59: #mark(natsFrom(X)) -> #mark(X) #60: #mark(U81(X1,X2,X3)) -> #a__U81(mark(X1),X2,X3) #61: #mark(U81(X1,X2,X3)) -> #mark(X1) #62: #a__splitAt(0(),XS) -> #mark(XS) #63: #a__fst(pair(X,Y)) -> #a__U21(tt(),X) #64: #a__U41(tt(),N,XS) -> #a__U42(tt(),N,XS) #65: #mark(head(X)) -> #a__head(mark(X)) #66: #mark(head(X)) -> #mark(X) #67: #a__U52(tt(),Y) -> #mark(Y) #68: #mark(U21(X1,X2)) -> #a__U21(mark(X1),X2) #69: #mark(U21(X1,X2)) -> #mark(X1) #70: #a__U31(tt(),N) -> #a__U32(tt(),N) #71: #mark(U62(X1,X2,X3,X4)) -> #a__U62(mark(X1),X2,X3,X4) #72: #mark(U62(X1,X2,X3,X4)) -> #mark(X1) #73: #a__take(N,XS) -> #a__U81(tt(),N,XS) #74: #a__natsFrom(N) -> #mark(N) #75: #mark(U22(X1,X2)) -> #a__U22(mark(X1),X2) #76: #mark(U22(X1,X2)) -> #mark(X1) #77: #a__tail(cons(N,XS)) -> #a__U71(tt(),XS) #78: #a__U81(tt(),N,XS) -> #a__U82(tt(),N,XS) #79: #mark(splitAt(X1,X2)) -> #a__splitAt(mark(X1),mark(X2)) #80: #mark(splitAt(X1,X2)) -> #mark(X1) #81: #mark(splitAt(X1,X2)) -> #mark(X2) #82: #a__afterNth(N,XS) -> #a__U11(tt(),N,XS) #83: #a__splitAt(s(N),cons(X,XS)) -> #a__U61(tt(),N,X,XS) #84: #mark(U32(X1,X2)) -> #a__U32(mark(X1),X2) #85: #mark(U32(X1,X2)) -> #mark(X1) #86: #a__head(cons(N,XS)) -> #a__U31(tt(),N) #87: #a__U72(tt(),XS) -> #mark(XS) #88: #a__U21(tt(),X) -> #a__U22(tt(),X) #89: #a__U11(tt(),N,XS) -> #a__U12(tt(),N,XS) #90: #mark(tail(X)) -> #a__tail(mark(X)) #91: #mark(tail(X)) -> #mark(X) #92: #a__U42(tt(),N,XS) -> #a__head(a__afterNth(mark(N),mark(XS))) #93: #a__U42(tt(),N,XS) -> #a__afterNth(mark(N),mark(XS)) #94: #a__U42(tt(),N,XS) -> #mark(N) #95: #a__U42(tt(),N,XS) -> #mark(XS) #96: #a__U71(tt(),XS) -> #a__U72(tt(),XS) #97: #a__U22(tt(),X) -> #mark(X) #98: #mark(U82(X1,X2,X3)) -> #a__U82(mark(X1),X2,X3) #99: #mark(U82(X1,X2,X3)) -> #mark(X1) #100: #a__U82(tt(),N,XS) -> #a__fst(a__splitAt(mark(N),mark(XS))) #101: #a__U82(tt(),N,XS) -> #a__splitAt(mark(N),mark(XS)) #102: #a__U82(tt(),N,XS) -> #mark(N) #103: #a__U82(tt(),N,XS) -> #mark(XS) Number of SCCs: 1, DPs: 103, edges: 3244 SCC { #1..103 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. a__U63(x1,x2,x3,x4) weight: max{(/ 242503 32) + x4, (/ 121255 16) + x3, (/ 242515 32) + x2, (/ 242499 32) + x1} U21(x1,x2) weight: max{(/ 3 8) + x2, (/ 7 32) + x1} #a__U82(x1,x2,x3) weight: max{0, (/ 121257 16) + x3, (/ 121263 16) + x2} #a__U72(x1,x2) weight: max{(/ 1 32) + x2, (/ 3 32) + x1} #a__U71(x1,x2) weight: max{(/ 5 16) + x2, (/ 5 16) + x1} U11(x1,x2,x3) weight: max{(/ 30317 4) + x3, (/ 121267 16) + x2, (/ 242533 32) + x1} U64(x1,x2) weight: max{(/ 242507 32) + x2, x1} s(x1) weight: x1 #a__U31(x1,x2) weight: max{(/ 5 32) + x2, (/ 1 16) + x1} #a__head(x1) weight: (/ 9 32) + x1 #a__natsFrom(x1) weight: (/ 1 32) + x1 #a__snd(x1) weight: (/ 5 16) + x1 a__afterNth(x1,x2) weight: max{(/ 242537 32) + x2, (/ 242539 32) + x1} U42(x1,x2,x3) weight: max{(/ 30319 4) + x3, (/ 121275 16) + x2, (/ 121279 16) + x1} a__U82(x1,x2,x3) weight: max{(/ 242525 32) + x3, (/ 242527 32) + x2, x1} take(x1,x2) weight: max{(/ 121265 16) + x2, (/ 242529 32) + x1} U71(x1,x2) weight: max{(/ 9 16) + x2, (/ 11 32) + x1} a__U62(x1,x2,x3,x4) weight: max{(/ 242503 32) + x4, (/ 121255 16) + x3, (/ 242515 32) + x2, (/ 242509 32) + x1} pair(x1,x2) weight: max{(/ 7 32) + x2, (/ 1 32) + x1} fst(x1) weight: (/ 11 32) + x1 natsFrom(x1) weight: (/ 1 4) + x1 a__snd(x1) weight: (/ 19 32) + x1 #a__U51(x1,x2) weight: max{(/ 1 2) + x2, (/ 1 8) + x1} U63(x1,x2,x3,x4) weight: max{(/ 242503 32) + x4, (/ 121255 16) + x3, (/ 242515 32) + x2, (/ 242499 32) + x1} a__U22(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} splitAt(x1,x2) weight: max{(/ 242503 32) + x2, (/ 242515 32) + x1} a__U64(x1,x2) weight: max{(/ 242507 32) + x2, x1} U72(x1,x2) weight: max{(/ 1 16) + x2, (/ 3 8) + x1} #a__U11(x1,x2,x3) weight: max{(/ 242535 32) + x3, (/ 60633 8) + x2, (/ 242531 32) + x1} a__U31(x1,x2) weight: max{(/ 19 32) + x2, (/ 3 16) + x1} a__U51(x1,x2) weight: max{(/ 5 8) + x2, (/ 15 32) + x1} a__U81(x1,x2,x3) weight: max{(/ 242529 32) + x3, (/ 242529 32) + x2, (/ 121259 16) + x1} #a__take(x1,x2) weight: max{7579 + x2, 7579 + x1} U12(x1,x2,x3) weight: max{(/ 121261 16) + x3, (/ 121267 16) + x2, (/ 242515 32) + x1} #a__U62(x1,x2,x3,x4) weight: max{0, (/ 242503 32) + x4, (/ 60627 8) + x3, (/ 242515 32) + x2} #a__U42(x1,x2,x3) weight: max{(/ 242551 32) + x3, (/ 242549 32) + x2, (/ 242553 32) + x1} a__U41(x1,x2,x3) weight: max{(/ 60641 8) + x3, (/ 60641 8) + x2, (/ 242561 32) + x1} #a__U64(x1,x2) weight: max{(/ 121253 16) + x2, x1} #a__U12(x1,x2,x3) weight: max{0, (/ 121257 16) + x3, (/ 121263 16) + x2} #a__U21(x1,x2) weight: max{(/ 1 4) + x2, (/ 1 8) + x1} #a__U81(x1,x2,x3) weight: max{(/ 242517 32) + x3, (/ 242527 32) + x2, (/ 1 32) + x1} #a__U61(x1,x2,x3,x4) weight: max{(/ 242503 32) + x4, (/ 121255 16) + x3, (/ 242515 32) + x2, (/ 242509 32) + x1} a__fst(x1) weight: (/ 11 32) + x1 a__natsFrom(x1) weight: (/ 1 4) + x1 tail(x1) weight: (/ 9 16) + x1 #mark(x1) weight: x1 0() weight: (/ 1 32) a__U21(x1,x2) weight: max{(/ 3 8) + x2, (/ 7 32) + x1} a__U32(x1,x2) weight: max{(/ 19 32) + x2, (/ 3 16) + x1} sel(x1,x2) weight: max{(/ 242567 32) + x2, (/ 60641 8) + x1} afterNth(x1,x2) weight: max{(/ 242537 32) + x2, (/ 242539 32) + x1} nil() weight: (/ 1 32) a__splitAt(x1,x2) weight: max{(/ 242503 32) + x2, (/ 242515 32) + x1} U62(x1,x2,x3,x4) weight: max{(/ 242503 32) + x4, (/ 121255 16) + x3, (/ 242515 32) + x2, (/ 242509 32) + x1} #a__U52(x1,x2) weight: max{(/ 1 32) + x2, (/ 3 32) + x1} #a__sel(x1,x2) weight: max{(/ 242565 32) + x2, (/ 242563 32) + x1} mark(x1) weight: x1 a__U72(x1,x2) weight: max{(/ 1 16) + x2, (/ 3 8) + x1} a__U11(x1,x2,x3) weight: max{(/ 30317 4) + x3, (/ 121267 16) + x2, (/ 242533 32) + x1} U32(x1,x2) weight: max{(/ 19 32) + x2, (/ 3 16) + x1} a__sel(x1,x2) weight: max{(/ 242567 32) + x2, (/ 60641 8) + x1} a__U42(x1,x2,x3) weight: max{(/ 30319 4) + x3, (/ 121275 16) + x2, (/ 121279 16) + x1} a__U52(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} a__U12(x1,x2,x3) weight: max{(/ 121261 16) + x3, (/ 121267 16) + x2, (/ 242515 32) + x1} #a__U63(x1,x2,x3,x4) weight: max{(/ 242503 32) + x4, (/ 242507 32) + x3, (/ 242515 32) + x2, (/ 242499 32) + x1} U52(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} U61(x1,x2,x3,x4) weight: max{(/ 242503 32) + x4, (/ 242511 32) + x3, (/ 242515 32) + x2, (/ 242509 32) + x1} #a__U22(x1,x2) weight: max{(/ 1 32) + x2, (/ 3 32) + x1} U31(x1,x2) weight: max{(/ 19 32) + x2, (/ 3 16) + x1} a__U71(x1,x2) weight: max{(/ 9 16) + x2, (/ 11 32) + x1} head(x1) weight: (/ 11 32) + x1 #a__afterNth(x1,x2) weight: max{(/ 30317 4) + x2, (/ 121269 16) + x1} #a__splitAt(x1,x2) weight: max{(/ 242503 32) + x2, (/ 242515 32) + x1} cons(x1,x2) weight: max{x2, (/ 1 4) + x1} a__U61(x1,x2,x3,x4) weight: max{(/ 242503 32) + x4, (/ 242511 32) + x3, (/ 242515 32) + x2, (/ 242509 32) + x1} snd(x1) weight: (/ 19 32) + x1 a__take(x1,x2) weight: max{(/ 121265 16) + x2, (/ 242529 32) + x1} U81(x1,x2,x3) weight: max{(/ 242529 32) + x3, (/ 242529 32) + x2, (/ 121259 16) + x1} #a__U41(x1,x2,x3) weight: max{0, (/ 121281 16) + x3, 7580 + x2} U82(x1,x2,x3) weight: max{(/ 242525 32) + x3, (/ 242527 32) + x2, x1} tt() weight: (/ 3 16) #a__fst(x1) weight: (/ 5 16) + x1 U22(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} U51(x1,x2) weight: max{(/ 5 8) + x2, (/ 15 32) + x1} a__tail(x1) weight: (/ 9 16) + x1 U41(x1,x2,x3) weight: max{(/ 60641 8) + x3, (/ 60641 8) + x2, (/ 242561 32) + x1} #a__tail(x1) weight: (/ 17 32) + x1 #a__U32(x1,x2) weight: max{(/ 1 32) + x2, (/ 1 32) + x1} a__head(x1) weight: (/ 11 32) + x1 Usable rules: { 1..88 } Removed DPs: #1..4 #6..10 #13..29 #31..38 #41..43 #45..48 #50 #52..70 #72..78 #80..82 #84..98 #100..103 Number of SCCs: 2, DPs: 7, edges: 13 SCC { #12 #30 #99 } Removing DPs: Order(PosReal,>,Sum)... succeeded. a__U63(x1,x2,x3,x4) weight: (/ 11 16) + x2 + x3 U21(x1,x2) weight: (/ 13 16) + x1 #a__U82(x1,x2,x3) weight: 0 #a__U72(x1,x2) weight: 0 #a__U71(x1,x2) weight: 0 U11(x1,x2,x3) weight: (/ 3 16) U64(x1,x2) weight: (/ 5 16) + x1 s(x1) weight: (/ 1 16) + x1 #a__U31(x1,x2) weight: 0 #a__head(x1) weight: 0 #a__natsFrom(x1) weight: 0 #a__snd(x1) weight: 0 a__afterNth(x1,x2) weight: (/ 1 16) U42(x1,x2,x3) weight: (/ 11 16) + x2 a__U82(x1,x2,x3) weight: (/ 5 8) + x1 + x2 take(x1,x2) weight: (/ 9 16) + x1 + x2 U71(x1,x2) weight: (/ 5 8) + x2 a__U62(x1,x2,x3,x4) weight: (/ 5 8) + x4 pair(x1,x2) weight: (/ 9 16) fst(x1) weight: (/ 3 4) natsFrom(x1) weight: (/ 9 16) a__snd(x1) weight: (/ 1 4) #a__U51(x1,x2) weight: 0 U63(x1,x2,x3,x4) weight: (/ 3 4) + x1 a__U22(x1,x2) weight: (/ 13 16) + x2 splitAt(x1,x2) weight: (/ 9 16) + x1 + x2 a__U64(x1,x2) weight: (/ 1 4) + x1 + x2 U72(x1,x2) weight: (/ 7 16) #a__U11(x1,x2,x3) weight: 0 a__U31(x1,x2) weight: (/ 3 4) + x2 a__U51(x1,x2) weight: (/ 5 16) + x1 a__U81(x1,x2,x3) weight: (/ 9 16) + x1 + x3 #a__take(x1,x2) weight: 0 U12(x1,x2,x3) weight: (/ 1 4) + x1 #a__U62(x1,x2,x3,x4) weight: 0 #a__U42(x1,x2,x3) weight: 0 a__U41(x1,x2,x3) weight: (/ 9 16) + x1 #a__U64(x1,x2) weight: 0 #a__U12(x1,x2,x3) weight: 0 #a__U21(x1,x2) weight: 0 #a__U81(x1,x2,x3) weight: 0 #a__U61(x1,x2,x3,x4) weight: 0 a__fst(x1) weight: (/ 11 16) a__natsFrom(x1) weight: (/ 1 2) tail(x1) weight: (/ 9 16) + x1 #mark(x1) weight: x1 0() weight: 0 a__U21(x1,x2) weight: (/ 3 4) + x2 a__U32(x1,x2) weight: (/ 13 16) sel(x1,x2) weight: (/ 9 16) + x2 afterNth(x1,x2) weight: (/ 1 8) + x1 + x2 nil() weight: 0 a__splitAt(x1,x2) weight: (/ 1 2) U62(x1,x2,x3,x4) weight: (/ 11 16) + x1 + x3 #a__U52(x1,x2) weight: 0 #a__sel(x1,x2) weight: 0 mark(x1) weight: (/ 7 16) a__U72(x1,x2) weight: (/ 3 8) + x1 + x2 a__U11(x1,x2,x3) weight: (/ 1 8) + x1 + x2 + x3 U32(x1,x2) weight: (/ 7 8) + x1 a__sel(x1,x2) weight: (/ 1 2) a__U42(x1,x2,x3) weight: (/ 5 8) + x1 + x3 a__U52(x1,x2) weight: (/ 3 8) + x1 a__U12(x1,x2,x3) weight: (/ 3 16) + x3 #a__U63(x1,x2,x3,x4) weight: 0 U52(x1,x2) weight: (/ 7 16) + x2 U61(x1,x2,x3,x4) weight: (/ 5 8) + x2 #a__U22(x1,x2) weight: 0 U31(x1,x2) weight: (/ 13 16) + x1 a__U71(x1,x2) weight: (/ 9 16) head(x1) weight: (/ 3 4) #a__afterNth(x1,x2) weight: 0 #a__splitAt(x1,x2) weight: 0 cons(x1,x2) weight: (/ 9 16) a__U61(x1,x2,x3,x4) weight: (/ 9 16) + x1 + x3 + x4 snd(x1) weight: (/ 5 16) a__take(x1,x2) weight: (/ 1 2) U81(x1,x2,x3) weight: (/ 5 8) #a__U41(x1,x2,x3) weight: 0 U82(x1,x2,x3) weight: (/ 11 16) + x1 + x3 tt() weight: 0 #a__fst(x1) weight: 0 U22(x1,x2) weight: (/ 7 8) U51(x1,x2) weight: (/ 3 8) a__tail(x1) weight: (/ 1 2) U41(x1,x2,x3) weight: (/ 5 8) + x2 + x3 #a__tail(x1) weight: 0 #a__U32(x1,x2) weight: 0 a__head(x1) weight: (/ 11 16) Usable rules: { } Removed DPs: #12 #30 #99 Number of SCCs: 1, DPs: 4, edges: 4 SCC { #40 #44 #51 #83 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. a__U63(x1,x2,x3,x4) weight: max{0, (/ 5 16) + x4, (/ 5 32) + x3, (/ 3 16) + x2} status: [x3,x2,x4] precedence above: U64 pair U63 a__U64 cons U21(x1,x2) weight: (/ 1 16) + x2 status: [] precedence above: a__U22 a__U21 U22 #a__U82(x1,x2,x3) weight: (/ 1 32) + x3 + x2 + x1 status: [x3,x2,x1] precedence above: #a__U72(x1,x2) weight: (/ 1 32) + x1 status: [x1] precedence above: #a__U71(x1,x2) weight: (/ 1 32) + x2 + x1 status: [x2,x1] precedence above: U11(x1,x2,x3) weight: (/ 15 32) + x3 + x2 status: [x2] precedence above: U21 U42 a__snd a__U22 a__U51 U12 a__U41 a__U21 sel mark a__U11 a__sel a__U42 a__U52 a__U12 U52 cons snd tt U22 U51 U41 U64(x1,x2) weight: max{(/ 5 32) + x2, x1} status: [] precedence above: pair a__U64 cons s(x1) weight: x1 status: [x1] precedence above: U21 U42 fst a__U22 a__U41 a__fst a__U21 sel mark a__sel a__U42 tt U22 U41 #a__U31(x1,x2) weight: x1 status: [] precedence above: #a__head(x1) weight: x1 status: [] precedence above: #a__natsFrom(x1) weight: (/ 1 32) status: [] precedence above: #a__snd(x1) weight: x1 status: [] precedence above: a__afterNth(x1,x2) weight: (/ 1 2) + x2 + x1 status: [x1] precedence above: U21 U11 U42 a__snd a__U22 a__U51 U12 a__U41 a__U21 sel afterNth mark a__U11 a__sel a__U42 a__U52 a__U12 U52 cons snd tt U22 U51 U41 U42(x1,x2,x3) weight: (/ 17 32) + x3 + x2 status: [] precedence above: a__U42 a__U82(x1,x2,x3) weight: (/ 3 8) + x3 + x2 status: [x2] precedence above: U21 fst a__U22 a__fst a__U21 U82 U22 take(x1,x2) weight: (/ 7 16) + x2 + x1 status: [] precedence above: U21 a__U82 fst a__U22 a__U81 a__fst a__U21 a__take U81 U82 U22 U71(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x1,x2] precedence above: a__U71 a__U62(x1,x2,x3,x4) weight: max{(/ 5 16) + x4, (/ 7 32) + x3, (/ 3 16) + x2, (/ 11 32) + x1} status: [x3,x2,x4,x1] precedence above: a__U63 U64 pair U63 a__U64 U62 cons pair(x1,x2) weight: max{x2, (/ 1 32) + x1} status: [] precedence above: fst(x1) weight: (/ 1 32) + x1 status: [] precedence above: U21 a__U22 a__fst a__U21 U22 natsFrom(x1) weight: (/ 1 8) + x1 status: [] precedence above: a__natsFrom cons a__snd(x1) weight: (/ 3 32) + x1 status: [] precedence above: U42 a__U51 a__U41 sel mark a__sel a__U42 a__U52 U52 cons snd tt U51 U41 #a__U51(x1,x2) weight: (/ 1 32) + x2 + x1 status: [x1,x2] precedence above: U63(x1,x2,x3,x4) weight: max{0, (/ 5 16) + x4, (/ 5 32) + x3, (/ 3 16) + x2} status: [x3,x2,x4] precedence above: a__U63 U64 pair a__U64 cons a__U22(x1,x2) weight: (/ 1 32) + x2 status: [] precedence above: U22 splitAt(x1,x2) weight: max{(/ 5 16) + x2, (/ 3 16) + x1} status: [] precedence above: a__U63 U64 a__U62 pair U63 a__U64 a__splitAt U62 U61 cons a__U61 a__U64(x1,x2) weight: max{(/ 5 32) + x2, x1} status: [] precedence above: U64 pair cons U72(x1,x2) weight: (/ 1 32) + x2 status: [] precedence above: a__U72 #a__U11(x1,x2,x3) weight: (/ 1 32) + x3 status: [x3] precedence above: a__U31(x1,x2) weight: (/ 1 16) + x2 status: [x2] precedence above: a__U32 U32 U31 a__U51(x1,x2) weight: (/ 1 16) + x2 status: [x2] precedence above: U42 a__U41 sel mark a__sel a__U42 a__U52 U52 cons tt U51 U41 a__U81(x1,x2,x3) weight: (/ 13 32) + x3 + x2 status: [x2] precedence above: U21 a__U82 fst a__U22 a__fst a__U21 U81 U82 U22 #a__take(x1,x2) weight: x2 status: [] precedence above: U12(x1,x2,x3) weight: (/ 7 16) + x3 + x2 status: [x2] precedence above: U21 U42 a__snd a__U22 a__U51 a__U41 a__U21 sel mark a__sel a__U42 a__U52 a__U12 U52 cons snd tt U22 U51 U41 #a__U62(x1,x2,x3,x4) weight: max{0, (/ 7 32) + x2, (/ 5 32) + x1} status: [x2,x1] precedence above: U21 U42 fst a__U22 a__U41 #a__U61 a__fst a__U21 sel mark a__sel a__U42 #a__U63 #a__splitAt tt U22 U41 #a__U42(x1,x2,x3) weight: x2 status: [] precedence above: a__U41(x1,x2,x3) weight: (/ 9 16) + x3 + x2 status: [] precedence above: U42 a__U42 U41 #a__U64(x1,x2) weight: x1 status: [x1] precedence above: #a__U12(x1,x2,x3) weight: (/ 1 32) + x3 + x2 + x1 status: [x3,x1,x2] precedence above: #a__U21(x1,x2) weight: (/ 1 32) + x1 status: [x1] precedence above: #a__U81(x1,x2,x3) weight: (/ 1 32) + x3 + x1 status: [x3,x1] precedence above: #a__U61(x1,x2,x3,x4) weight: max{0, (/ 7 32) + x2, (/ 1 8) + x1} status: [x2,x1] precedence above: U21 U42 fst a__U22 #a__U62 a__U41 a__fst a__U21 sel mark a__sel a__U42 #a__U63 #a__splitAt tt U22 U41 a__fst(x1) weight: (/ 1 32) + x1 status: [] precedence above: U21 fst a__U22 a__U21 U22 a__natsFrom(x1) weight: (/ 1 8) + x1 status: [] precedence above: natsFrom cons tail(x1) weight: (/ 5 32) + x1 status: [] precedence above: a__tail #mark(x1) weight: (/ 1 32) status: [] precedence above: 0() weight: (/ 1 32) status: [] precedence above: a__U21(x1,x2) weight: (/ 1 16) + x2 status: [] precedence above: U21 a__U22 U22 a__U32(x1,x2) weight: (/ 1 32) + x2 status: [x2] precedence above: U32 sel(x1,x2) weight: (/ 19 32) + x2 + x1 status: [] precedence above: U42 a__U41 a__sel a__U42 U41 afterNth(x1,x2) weight: (/ 1 2) + x2 + x1 status: [x1] precedence above: U21 U11 a__afterNth U42 a__snd a__U22 a__U51 U12 a__U41 a__U21 sel mark a__U11 a__sel a__U42 a__U52 a__U12 U52 cons snd tt U22 U51 U41 nil() weight: (/ 1 4) status: [] precedence above: a__splitAt(x1,x2) weight: max{(/ 5 16) + x2, (/ 3 16) + x1} status: [] precedence above: a__U63 U64 a__U62 pair U63 splitAt a__U64 U62 U61 cons a__U61 U62(x1,x2,x3,x4) weight: max{(/ 5 16) + x4, (/ 7 32) + x3, (/ 3 16) + x2, (/ 11 32) + x1} status: [x3,x2,x4,x1] precedence above: a__U63 U64 a__U62 pair U63 a__U64 cons #a__U52(x1,x2) weight: (/ 1 32) + x2 + x1 status: [x1,x2] precedence above: #a__sel(x1,x2) weight: (/ 1 32) + x2 + x1 status: [x2,x1] precedence above: mark(x1) weight: x1 status: x1 a__U72(x1,x2) weight: (/ 1 32) + x2 status: [] precedence above: U72 a__U11(x1,x2,x3) weight: (/ 15 32) + x3 + x2 status: [x2] precedence above: U21 U11 U42 a__snd a__U22 a__U51 U12 a__U41 a__U21 sel mark a__sel a__U42 a__U52 a__U12 U52 cons snd tt U22 U51 U41 U32(x1,x2) weight: (/ 1 32) + x2 status: [x2] precedence above: a__U32 a__sel(x1,x2) weight: (/ 19 32) + x2 + x1 status: [] precedence above: U42 a__U41 sel a__U42 U41 a__U42(x1,x2,x3) weight: (/ 17 32) + x3 + x2 status: [] precedence above: U42 a__U52(x1,x2) weight: x2 status: x2 a__U12(x1,x2,x3) weight: (/ 7 16) + x3 + x2 status: [x2] precedence above: U21 U42 a__snd a__U22 a__U51 U12 a__U41 a__U21 sel mark a__sel a__U42 a__U52 U52 cons snd tt U22 U51 U41 #a__U63(x1,x2,x3,x4) weight: max{0, (/ 7 32) + x2, (/ 3 16) + x1} status: [x2,x1] precedence above: U21 U42 fst a__U22 #a__U62 a__U41 #a__U61 a__fst a__U21 sel mark a__sel a__U42 #a__splitAt tt U22 U41 U52(x1,x2) weight: x2 status: x2 U61(x1,x2,x3,x4) weight: max{(/ 5 16) + x4, (/ 3 8) + x3, (/ 3 16) + x2, (/ 1 32) + x1} status: [x3,x2,x4,x1] precedence above: a__U63 U64 a__U62 pair U63 a__U64 U62 cons a__U61 #a__U22(x1,x2) weight: (/ 1 32) + x1 status: [x1] precedence above: U31(x1,x2) weight: (/ 1 16) + x2 status: [x2] precedence above: a__U31 a__U32 U32 a__U71(x1,x2) weight: (/ 1 8) + x2 + x1 status: [x1,x2] precedence above: U71 head(x1) weight: x1 status: x1 #a__afterNth(x1,x2) weight: (/ 1 32) + x2 + x1 status: [x1,x2] precedence above: #a__splitAt(x1,x2) weight: max{0, (/ 7 32) + x1} status: [x1] precedence above: U21 U42 fst a__U22 #a__U62 a__U41 #a__U61 a__fst a__U21 sel mark a__sel a__U42 #a__U63 tt U22 U41 cons(x1,x2) weight: max{x2, (/ 3 32) + x1} status: [] precedence above: a__U61(x1,x2,x3,x4) weight: max{(/ 5 16) + x4, (/ 3 8) + x3, (/ 3 16) + x2, (/ 1 32) + x1} status: [x3,x2,x4,x1] precedence above: a__U63 U64 a__U62 pair U63 a__U64 U62 U61 cons snd(x1) weight: (/ 3 32) + x1 status: [] precedence above: U42 a__snd a__U51 a__U41 sel mark a__sel a__U42 a__U52 U52 cons tt U51 U41 a__take(x1,x2) weight: (/ 7 16) + x2 + x1 status: [] precedence above: U21 a__U82 take fst a__U22 a__U81 a__fst a__U21 U81 U82 U22 U81(x1,x2,x3) weight: (/ 13 32) + x3 + x2 status: [x2] precedence above: U21 a__U82 fst a__U22 a__U81 a__fst a__U21 U82 U22 #a__U41(x1,x2,x3) weight: (/ 1 32) + x3 + x2 + x1 status: [x1,x2,x3] precedence above: U82(x1,x2,x3) weight: (/ 3 8) + x3 + x2 status: [x2] precedence above: U21 a__U82 fst a__U22 a__fst a__U21 U22 tt() weight: 0 status: [] precedence above: U42 a__U41 a__U42 U41 #a__fst(x1) weight: x1 status: [] precedence above: U22(x1,x2) weight: (/ 1 32) + x2 status: [] precedence above: a__U22 U51(x1,x2) weight: (/ 1 16) + x2 status: [x2] precedence above: U42 a__U51 a__U41 sel mark a__sel a__U42 a__U52 U52 cons tt U41 a__tail(x1) weight: (/ 5 32) + x1 status: [] precedence above: tail U41(x1,x2,x3) weight: (/ 9 16) + x3 + x2 status: [] precedence above: U42 a__U41 a__U42 #a__tail(x1) weight: (/ 1 32) status: [] precedence above: #a__U32(x1,x2) weight: (/ 1 32) + x2 + x1 status: [x1,x2] precedence above: a__head(x1) weight: x1 status: x1 Usable rules: { 1..88 } Removed DPs: #40 #83 Number of SCCs: 0, DPs: 0, edges: 0 YES