Input TRS: 1: a__U101(tt(),N,XS) -> a__fst(a__splitAt(mark(N),mark(XS))) 2: a__U11(tt(),N,XS) -> a__snd(a__splitAt(mark(N),mark(XS))) 3: a__U21(tt(),X) -> mark(X) 4: a__U31(tt(),N) -> mark(N) 5: a__U41(tt(),N) -> cons(mark(N),natsFrom(s(N))) 6: a__U51(tt(),N,XS) -> a__head(a__afterNth(mark(N),mark(XS))) 7: a__U61(tt(),Y) -> mark(Y) 8: a__U71(tt(),XS) -> pair(nil(),mark(XS)) 9: a__U81(tt(),N,X,XS) -> a__U82(a__splitAt(mark(N),mark(XS)),X) 10: a__U82(pair(YS,ZS),X) -> pair(cons(mark(X),YS),mark(ZS)) 11: a__U91(tt(),XS) -> mark(XS) 12: a__afterNth(N,XS) -> a__U11(a__and(a__isNatural(N),isLNat(XS)),N,XS) 13: a__and(tt(),X) -> mark(X) 14: a__fst(pair(X,Y)) -> a__U21(a__and(a__isLNat(X),isLNat(Y)),X) 15: a__head(cons(N,XS)) -> a__U31(a__and(a__isNatural(N),isLNat(XS)),N) 16: a__isLNat(nil()) -> tt() 17: a__isLNat(afterNth(V1,V2)) -> a__and(a__isNatural(V1),isLNat(V2)) 18: a__isLNat(cons(V1,V2)) -> a__and(a__isNatural(V1),isLNat(V2)) 19: a__isLNat(fst(V1)) -> a__isPLNat(V1) 20: a__isLNat(natsFrom(V1)) -> a__isNatural(V1) 21: a__isLNat(snd(V1)) -> a__isPLNat(V1) 22: a__isLNat(tail(V1)) -> a__isLNat(V1) 23: a__isLNat(take(V1,V2)) -> a__and(a__isNatural(V1),isLNat(V2)) 24: a__isNatural(0()) -> tt() 25: a__isNatural(head(V1)) -> a__isLNat(V1) 26: a__isNatural(s(V1)) -> a__isNatural(V1) 27: a__isNatural(sel(V1,V2)) -> a__and(a__isNatural(V1),isLNat(V2)) 28: a__isPLNat(pair(V1,V2)) -> a__and(a__isLNat(V1),isLNat(V2)) 29: a__isPLNat(splitAt(V1,V2)) -> a__and(a__isNatural(V1),isLNat(V2)) 30: a__natsFrom(N) -> a__U41(a__isNatural(N),N) 31: a__sel(N,XS) -> a__U51(a__and(a__isNatural(N),isLNat(XS)),N,XS) 32: a__snd(pair(X,Y)) -> a__U61(a__and(a__isLNat(X),isLNat(Y)),Y) 33: a__splitAt(0(),XS) -> a__U71(a__isLNat(XS),XS) 34: a__splitAt(s(N),cons(X,XS)) -> a__U81(a__and(a__isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS) 35: a__tail(cons(N,XS)) -> a__U91(a__and(a__isNatural(N),isLNat(XS)),XS) 36: a__take(N,XS) -> a__U101(a__and(a__isNatural(N),isLNat(XS)),N,XS) 37: mark(U101(X1,X2,X3)) -> a__U101(mark(X1),X2,X3) 38: mark(fst(X)) -> a__fst(mark(X)) 39: mark(splitAt(X1,X2)) -> a__splitAt(mark(X1),mark(X2)) 40: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) 41: mark(snd(X)) -> a__snd(mark(X)) 42: mark(U21(X1,X2)) -> a__U21(mark(X1),X2) 43: mark(U31(X1,X2)) -> a__U31(mark(X1),X2) 44: mark(U41(X1,X2)) -> a__U41(mark(X1),X2) 45: mark(natsFrom(X)) -> a__natsFrom(mark(X)) 46: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) 47: mark(head(X)) -> a__head(mark(X)) 48: mark(afterNth(X1,X2)) -> a__afterNth(mark(X1),mark(X2)) 49: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) 50: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) 51: mark(U81(X1,X2,X3,X4)) -> a__U81(mark(X1),X2,X3,X4) 52: mark(U82(X1,X2)) -> a__U82(mark(X1),X2) 53: mark(U91(X1,X2)) -> a__U91(mark(X1),X2) 54: mark(and(X1,X2)) -> a__and(mark(X1),X2) 55: mark(isNatural(X)) -> a__isNatural(X) 56: mark(isLNat(X)) -> a__isLNat(X) 57: mark(isPLNat(X)) -> a__isPLNat(X) 58: mark(tail(X)) -> a__tail(mark(X)) 59: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) 60: mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) 61: mark(tt()) -> tt() 62: mark(cons(X1,X2)) -> cons(mark(X1),X2) 63: mark(s(X)) -> s(mark(X)) 64: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2)) 65: mark(nil()) -> nil() 66: mark(0()) -> 0() 67: a__U101(X1,X2,X3) -> U101(X1,X2,X3) 68: a__fst(X) -> fst(X) 69: a__splitAt(X1,X2) -> splitAt(X1,X2) 70: a__U11(X1,X2,X3) -> U11(X1,X2,X3) 71: a__snd(X) -> snd(X) 72: a__U21(X1,X2) -> U21(X1,X2) 73: a__U31(X1,X2) -> U31(X1,X2) 74: a__U41(X1,X2) -> U41(X1,X2) 75: a__natsFrom(X) -> natsFrom(X) 76: a__U51(X1,X2,X3) -> U51(X1,X2,X3) 77: a__head(X) -> head(X) 78: a__afterNth(X1,X2) -> afterNth(X1,X2) 79: a__U61(X1,X2) -> U61(X1,X2) 80: a__U71(X1,X2) -> U71(X1,X2) 81: a__U81(X1,X2,X3,X4) -> U81(X1,X2,X3,X4) 82: a__U82(X1,X2) -> U82(X1,X2) 83: a__U91(X1,X2) -> U91(X1,X2) 84: a__and(X1,X2) -> and(X1,X2) 85: a__isNatural(X) -> isNatural(X) 86: a__isLNat(X) -> isLNat(X) 87: a__isPLNat(X) -> isPLNat(X) 88: a__tail(X) -> tail(X) 89: a__take(X1,X2) -> take(X1,X2) 90: a__sel(X1,X2) -> sel(X1,X2) Number of strict rules: 90 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #a__U11(tt(),N,XS) -> #a__snd(a__splitAt(mark(N),mark(XS))) #2: #a__U11(tt(),N,XS) -> #a__splitAt(mark(N),mark(XS)) #3: #a__U11(tt(),N,XS) -> #mark(N) #4: #a__U11(tt(),N,XS) -> #mark(XS) #5: #mark(U31(X1,X2)) -> #a__U31(mark(X1),X2) #6: #mark(U31(X1,X2)) -> #mark(X1) #7: #a__isPLNat(splitAt(V1,V2)) -> #a__and(a__isNatural(V1),isLNat(V2)) #8: #a__isPLNat(splitAt(V1,V2)) -> #a__isNatural(V1) #9: #a__tail(cons(N,XS)) -> #a__U91(a__and(a__isNatural(N),isLNat(XS)),XS) #10: #a__tail(cons(N,XS)) -> #a__and(a__isNatural(N),isLNat(XS)) #11: #a__tail(cons(N,XS)) -> #a__isNatural(N) #12: #mark(U51(X1,X2,X3)) -> #a__U51(mark(X1),X2,X3) #13: #mark(U51(X1,X2,X3)) -> #mark(X1) #14: #mark(U21(X1,X2)) -> #a__U21(mark(X1),X2) #15: #mark(U21(X1,X2)) -> #mark(X1) #16: #mark(snd(X)) -> #a__snd(mark(X)) #17: #mark(snd(X)) -> #mark(X) #18: #mark(U101(X1,X2,X3)) -> #a__U101(mark(X1),X2,X3) #19: #mark(U101(X1,X2,X3)) -> #mark(X1) #20: #mark(head(X)) -> #a__head(mark(X)) #21: #mark(head(X)) -> #mark(X) #22: #mark(U91(X1,X2)) -> #a__U91(mark(X1),X2) #23: #mark(U91(X1,X2)) -> #mark(X1) #24: #mark(afterNth(X1,X2)) -> #a__afterNth(mark(X1),mark(X2)) #25: #mark(afterNth(X1,X2)) -> #mark(X1) #26: #mark(afterNth(X1,X2)) -> #mark(X2) #27: #mark(tail(X)) -> #a__tail(mark(X)) #28: #mark(tail(X)) -> #mark(X) #29: #mark(fst(X)) -> #a__fst(mark(X)) #30: #mark(fst(X)) -> #mark(X) #31: #a__U51(tt(),N,XS) -> #a__head(a__afterNth(mark(N),mark(XS))) #32: #a__U51(tt(),N,XS) -> #a__afterNth(mark(N),mark(XS)) #33: #a__U51(tt(),N,XS) -> #mark(N) #34: #a__U51(tt(),N,XS) -> #mark(XS) #35: #mark(take(X1,X2)) -> #a__take(mark(X1),mark(X2)) #36: #mark(take(X1,X2)) -> #mark(X1) #37: #mark(take(X1,X2)) -> #mark(X2) #38: #mark(isNatural(X)) -> #a__isNatural(X) #39: #mark(U11(X1,X2,X3)) -> #a__U11(mark(X1),X2,X3) #40: #mark(U11(X1,X2,X3)) -> #mark(X1) #41: #mark(U81(X1,X2,X3,X4)) -> #a__U81(mark(X1),X2,X3,X4) #42: #mark(U81(X1,X2,X3,X4)) -> #mark(X1) #43: #a__and(tt(),X) -> #mark(X) #44: #a__U81(tt(),N,X,XS) -> #a__U82(a__splitAt(mark(N),mark(XS)),X) #45: #a__U81(tt(),N,X,XS) -> #a__splitAt(mark(N),mark(XS)) #46: #a__U81(tt(),N,X,XS) -> #mark(N) #47: #a__U81(tt(),N,X,XS) -> #mark(XS) #48: #a__U91(tt(),XS) -> #mark(XS) #49: #mark(isPLNat(X)) -> #a__isPLNat(X) #50: #a__isLNat(take(V1,V2)) -> #a__and(a__isNatural(V1),isLNat(V2)) #51: #a__isLNat(take(V1,V2)) -> #a__isNatural(V1) #52: #mark(natsFrom(X)) -> #a__natsFrom(mark(X)) #53: #mark(natsFrom(X)) -> #mark(X) #54: #a__afterNth(N,XS) -> #a__U11(a__and(a__isNatural(N),isLNat(XS)),N,XS) #55: #a__afterNth(N,XS) -> #a__and(a__isNatural(N),isLNat(XS)) #56: #a__afterNth(N,XS) -> #a__isNatural(N) #57: #a__sel(N,XS) -> #a__U51(a__and(a__isNatural(N),isLNat(XS)),N,XS) #58: #a__sel(N,XS) -> #a__and(a__isNatural(N),isLNat(XS)) #59: #a__sel(N,XS) -> #a__isNatural(N) #60: #mark(isLNat(X)) -> #a__isLNat(X) #61: #a__fst(pair(X,Y)) -> #a__U21(a__and(a__isLNat(X),isLNat(Y)),X) #62: #a__fst(pair(X,Y)) -> #a__and(a__isLNat(X),isLNat(Y)) #63: #a__fst(pair(X,Y)) -> #a__isLNat(X) #64: #mark(cons(X1,X2)) -> #mark(X1) #65: #a__natsFrom(N) -> #a__U41(a__isNatural(N),N) #66: #a__natsFrom(N) -> #a__isNatural(N) #67: #mark(U82(X1,X2)) -> #a__U82(mark(X1),X2) #68: #mark(U82(X1,X2)) -> #mark(X1) #69: #mark(U61(X1,X2)) -> #a__U61(mark(X1),X2) #70: #mark(U61(X1,X2)) -> #mark(X1) #71: #a__isNatural(head(V1)) -> #a__isLNat(V1) #72: #a__isLNat(natsFrom(V1)) -> #a__isNatural(V1) #73: #a__U61(tt(),Y) -> #mark(Y) #74: #mark(splitAt(X1,X2)) -> #a__splitAt(mark(X1),mark(X2)) #75: #mark(splitAt(X1,X2)) -> #mark(X1) #76: #mark(splitAt(X1,X2)) -> #mark(X2) #77: #a__U82(pair(YS,ZS),X) -> #mark(X) #78: #a__U82(pair(YS,ZS),X) -> #mark(ZS) #79: #mark(pair(X1,X2)) -> #mark(X1) #80: #mark(pair(X1,X2)) -> #mark(X2) #81: #a__splitAt(0(),XS) -> #a__U71(a__isLNat(XS),XS) #82: #a__splitAt(0(),XS) -> #a__isLNat(XS) #83: #a__U41(tt(),N) -> #mark(N) #84: #mark(U41(X1,X2)) -> #a__U41(mark(X1),X2) #85: #mark(U41(X1,X2)) -> #mark(X1) #86: #a__isPLNat(pair(V1,V2)) -> #a__and(a__isLNat(V1),isLNat(V2)) #87: #a__isPLNat(pair(V1,V2)) -> #a__isLNat(V1) #88: #a__isLNat(tail(V1)) -> #a__isLNat(V1) #89: #a__splitAt(s(N),cons(X,XS)) -> #a__U81(a__and(a__isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS) #90: #a__splitAt(s(N),cons(X,XS)) -> #a__and(a__isNatural(N),and(isNatural(X),isLNat(XS))) #91: #a__splitAt(s(N),cons(X,XS)) -> #a__isNatural(N) #92: #a__isNatural(sel(V1,V2)) -> #a__and(a__isNatural(V1),isLNat(V2)) #93: #a__isNatural(sel(V1,V2)) -> #a__isNatural(V1) #94: #mark(sel(X1,X2)) -> #a__sel(mark(X1),mark(X2)) #95: #mark(sel(X1,X2)) -> #mark(X1) #96: #mark(sel(X1,X2)) -> #mark(X2) #97: #a__isLNat(afterNth(V1,V2)) -> #a__and(a__isNatural(V1),isLNat(V2)) #98: #a__isLNat(afterNth(V1,V2)) -> #a__isNatural(V1) #99: #a__snd(pair(X,Y)) -> #a__U61(a__and(a__isLNat(X),isLNat(Y)),Y) #100: #a__snd(pair(X,Y)) -> #a__and(a__isLNat(X),isLNat(Y)) #101: #a__snd(pair(X,Y)) -> #a__isLNat(X) #102: #a__isLNat(fst(V1)) -> #a__isPLNat(V1) #103: #mark(s(X)) -> #mark(X) #104: #a__isNatural(s(V1)) -> #a__isNatural(V1) #105: #a__take(N,XS) -> #a__U101(a__and(a__isNatural(N),isLNat(XS)),N,XS) #106: #a__take(N,XS) -> #a__and(a__isNatural(N),isLNat(XS)) #107: #a__take(N,XS) -> #a__isNatural(N) #108: #a__isLNat(snd(V1)) -> #a__isPLNat(V1) #109: #a__U21(tt(),X) -> #mark(X) #110: #a__U101(tt(),N,XS) -> #a__fst(a__splitAt(mark(N),mark(XS))) #111: #a__U101(tt(),N,XS) -> #a__splitAt(mark(N),mark(XS)) #112: #a__U101(tt(),N,XS) -> #mark(N) #113: #a__U101(tt(),N,XS) -> #mark(XS) #114: #mark(and(X1,X2)) -> #a__and(mark(X1),X2) #115: #mark(and(X1,X2)) -> #mark(X1) #116: #a__U71(tt(),XS) -> #mark(XS) #117: #a__head(cons(N,XS)) -> #a__U31(a__and(a__isNatural(N),isLNat(XS)),N) #118: #a__head(cons(N,XS)) -> #a__and(a__isNatural(N),isLNat(XS)) #119: #a__head(cons(N,XS)) -> #a__isNatural(N) #120: #a__U31(tt(),N) -> #mark(N) #121: #mark(U71(X1,X2)) -> #a__U71(mark(X1),X2) #122: #mark(U71(X1,X2)) -> #mark(X1) #123: #a__isLNat(cons(V1,V2)) -> #a__and(a__isNatural(V1),isLNat(V2)) #124: #a__isLNat(cons(V1,V2)) -> #a__isNatural(V1) Number of SCCs: 1, DPs: 124, edges: 2698 SCC { #1..124 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. U21(x1,x2) weight: max{41076 + x2, (/ 328607 8) + x1} #a__U82(x1,x2) weight: max{41076 + x2, (/ 1 8) + x1} #a__U71(x1,x2) weight: max{0, 41076 + x2} U11(x1,x2,x3) weight: max{(/ 492907 8) + x3, (/ 123227 2) + x2, (/ 492909 8) + x1} s(x1) weight: x1 #a__U31(x1,x2) weight: max{0, 41076 + x2} #a__head(x1) weight: (/ 123227 2) + x1 #a__natsFrom(x1) weight: (/ 123227 2) + x1 isPLNat(x1) weight: (/ 41075 2) #a__snd(x1) weight: (/ 164303 4) + x1 a__afterNth(x1,x2) weight: max{(/ 657209 8) + x2, (/ 328605 4) + x1} U91(x1,x2) weight: max{(/ 82151 4) + x2, (/ 164303 8) + x1} a__U82(x1,x2) weight: max{(/ 657207 8) + x2, x1} take(x1,x2) weight: max{(/ 328605 4) + x2, (/ 657209 8) + x1} U71(x1,x2) weight: max{(/ 246453 4) + x2, (/ 1 4) + x1} and(x1,x2) weight: max{x2, x1} U101(x1,x2,x3) weight: max{(/ 492907 8) + x3, (/ 123227 2) + x2, (/ 492909 8) + x1} pair(x1,x2) weight: max{(/ 246453 4) + x2, (/ 492905 8) + x1} fst(x1) weight: (/ 1 8) + x1 natsFrom(x1) weight: (/ 82151 4) + x1 a__snd(x1) weight: (/ 1 8) + x1 #a__U51(x1,x2,x3) weight: max{0, (/ 1150119 8) + x3, (/ 1150119 8) + x2} splitAt(x1,x2) weight: max{(/ 246453 4) + x2, 61613 + x1} #a__U11(x1,x2,x3) weight: max{0, (/ 821513 8) + x3, (/ 821513 8) + x2} a__U31(x1,x2) weight: max{(/ 328603 8) + x2, (/ 82151 2) + x1} a__U51(x1,x2,x3) weight: max{(/ 985811 8) + x3, (/ 246453 2) + x2, (/ 821513 8) + x1} a__U81(x1,x2,x3,x4) weight: max{(/ 246453 4) + x4, (/ 657207 8) + x3, 61613 + x2, (/ 82151 2) + x1} #a__take(x1,x2) weight: max{(/ 492911 8) + x2, (/ 492911 8) + x1} isNatural(x1) weight: (/ 41075 2) a__U41(x1,x2) weight: max{(/ 82151 4) + x2, (/ 1 4) + x1} #a__U21(x1,x2) weight: max{0, (/ 492907 8) + x2} #a__U81(x1,x2,x3,x4) weight: max{0, (/ 123227 2) + x4, (/ 328605 4) + x3, (/ 492909 8) + x2} #a__U61(x1,x2) weight: max{0, 41076 + x2} a__fst(x1) weight: (/ 1 8) + x1 tail(x1) weight: (/ 328603 8) + x1 a__natsFrom(x1) weight: (/ 82151 4) + x1 #mark(x1) weight: (/ 328607 8) + x1 0() weight: (/ 1 8) #a__and(x1,x2) weight: max{0, (/ 328607 8) + x2} a__isLNat(x1) weight: (/ 41075 2) a__U21(x1,x2) weight: max{41076 + x2, (/ 328607 8) + x1} a__U91(x1,x2) weight: max{(/ 82151 4) + x2, (/ 164303 8) + x1} sel(x1,x2) weight: max{(/ 985813 8) + x2, (/ 246453 2) + x1} afterNth(x1,x2) weight: max{(/ 657209 8) + x2, (/ 328605 4) + x1} nil() weight: (/ 1 8) a__splitAt(x1,x2) weight: max{(/ 246453 4) + x2, 61613 + x1} isLNat(x1) weight: (/ 41075 2) #a__sel(x1,x2) weight: max{143765 + x2, 143765 + x1} mark(x1) weight: x1 #a__isLNat(x1) weight: (/ 492907 8) #a__U101(x1,x2,x3) weight: max{0, (/ 246455 4) + x3, (/ 246455 4) + x2} a__U11(x1,x2,x3) weight: max{(/ 492907 8) + x3, (/ 123227 2) + x2, (/ 492909 8) + x1} a__sel(x1,x2) weight: max{(/ 985813 8) + x2, (/ 246453 2) + x1} a__isPLNat(x1) weight: (/ 41075 2) U61(x1,x2) weight: max{(/ 1 4) + x2, (/ 3 8) + x1} U31(x1,x2) weight: max{(/ 328603 8) + x2, (/ 82151 2) + x1} a__U71(x1,x2) weight: max{(/ 246453 4) + x2, (/ 1 4) + x1} #a__isPLNat(x1) weight: (/ 492907 8) head(x1) weight: (/ 164301 4) + x1 #a__afterNth(x1,x2) weight: max{(/ 410757 4) + x2, (/ 410757 4) + x1} #a__splitAt(x1,x2) weight: max{(/ 123227 2) + x2, (/ 492909 8) + x1} cons(x1,x2) weight: max{x2, (/ 82151 4) + x1} a__U61(x1,x2) weight: max{(/ 1 4) + x2, (/ 3 8) + x1} snd(x1) weight: (/ 1 8) + x1 a__take(x1,x2) weight: max{(/ 328605 4) + x2, (/ 657209 8) + x1} U81(x1,x2,x3,x4) weight: max{(/ 246453 4) + x4, (/ 657207 8) + x3, 61613 + x2, (/ 82151 2) + x1} #a__U41(x1,x2) weight: max{0, 41076 + x2} U82(x1,x2) weight: max{(/ 657207 8) + x2, x1} tt() weight: (/ 164297 8) a__isNatural(x1) weight: (/ 41075 2) #a__isNatural(x1) weight: (/ 492907 8) #a__fst(x1) weight: (/ 3 8) + x1 U51(x1,x2,x3) weight: max{(/ 985811 8) + x3, (/ 246453 2) + x2, (/ 821513 8) + x1} a__and(x1,x2) weight: max{x2, x1} a__tail(x1) weight: (/ 328603 8) + x1 U41(x1,x2) weight: max{(/ 82151 4) + x2, (/ 1 4) + x1} #a__tail(x1) weight: (/ 123227 2) + x1 a__U101(x1,x2,x3) weight: max{(/ 492907 8) + x3, (/ 123227 2) + x2, (/ 492909 8) + x1} #a__U91(x1,x2) weight: max{0, (/ 123227 2) + x2} a__head(x1) weight: (/ 164301 4) + x1 Usable rules: { 1..90 } Removed DPs: #1..6 #10..37 #39..42 #44 #46..48 #52..59 #61..67 #69 #70 #73..85 #90 #91 #94..96 #99..101 #105..107 #109..113 #116..122 Number of SCCs: 2, DPs: 28, edges: 121 SCC { #45 #89 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded. U21(x1,x2) weight: max{0, (/ 288069 16) + x2} status: [] precedence above: U11 isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head cons a__U61 snd U81 U82 tt a__isNatural U51 a__head #a__U82(x1,x2) weight: (/ 1 16) + x2 status: [x2] precedence above: #a__U71(x1,x2) weight: (/ 1 16) + x2 status: [x2] precedence above: U11(x1,x2,x3) weight: max{(/ 36009 2) + x3, (/ 1 16) + x2, (/ 144035 8) + x1} status: [x1,x3] precedence above: a__U11 s(x1) weight: x1 status: [x1] precedence above: U21 U11 isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural #a__U81 a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head #a__splitAt cons a__U61 snd U81 U82 tt a__isNatural U51 a__head #a__U31(x1,x2) weight: (/ 1 16) + x2 + x1 status: [x1,x2] precedence above: #a__head(x1) weight: x1 status: [] precedence above: #a__natsFrom(x1) weight: x1 status: [] precedence above: isPLNat(x1) weight: 0 status: [] precedence above: U21 U11 U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head cons a__U61 snd U81 U82 tt a__isNatural U51 a__head #a__snd(x1) weight: x1 status: [] precedence above: a__afterNth(x1,x2) weight: max{(/ 288073 16) + x2, (/ 288069 16) + x1} status: [x2,x1] precedence above: U11 afterNth a__U11 U91(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 8) + x1} status: [] precedence above: U21 U11 isPLNat a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head cons a__U61 snd U81 U82 tt a__isNatural U51 a__head a__U82(x1,x2) weight: max{(/ 36009 2) + x2, x1} status: [] precedence above: pair U61 a__U61 U82 take(x1,x2) weight: (/ 288073 16) + x2 status: [] precedence above: U21 U11 s isPLNat U91 a__U82 U71 U101 pair fst a__snd splitAt a__U31 a__U51 a__U81 isNatural #a__U81 a__fst a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head #a__splitAt cons a__U61 snd a__take U81 U82 tt a__isNatural U51 a__U101 a__head U71(x1,x2) weight: max{0, (/ 144035 8) + x2} status: [] precedence above: pair U61 a__U71 a__U61 and(x1,x2) weight: max{0, x2} status: x2 U101(x1,x2,x3) weight: max{0, (/ 288073 16) + x3} status: [] precedence above: U21 U11 s isPLNat U91 a__U82 U71 pair fst a__snd splitAt a__U31 a__U51 a__U81 isNatural #a__U81 a__fst a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head #a__splitAt cons a__U61 snd U81 U82 tt a__isNatural U51 a__U101 a__head pair(x1,x2) weight: max{(/ 288069 16) + x2, (/ 288067 16) + x1} status: [] precedence above: U61 a__U61 fst(x1) weight: (/ 1 8) + x1 status: [] precedence above: U21 U11 s isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural #a__U81 a__fst a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head #a__splitAt cons a__U61 snd U81 U82 tt a__isNatural U51 a__head natsFrom(x1) weight: (/ 3 16) + x1 status: [] precedence above: a__U41 a__natsFrom cons tt U41 a__snd(x1) weight: x1 status: x1 #a__U51(x1,x2,x3) weight: (/ 1 16) + x3 + x2 + x1 status: [x2,x1,x3] precedence above: splitAt(x1,x2) weight: max{0, (/ 288071 16) + x2} status: [] precedence above: a__U82 U71 pair a__U81 a__splitAt U61 a__U71 a__U61 U81 U82 #a__U11(x1,x2,x3) weight: x3 status: [] precedence above: a__U31(x1,x2) weight: max{(/ 1 8) + x2, (/ 1 16) + x1} status: [] precedence above: U31 a__U51(x1,x2,x3) weight: max{(/ 288079 16) + x3, (/ 144039 8) + x2, (/ 288077 16) + x1} status: [x2] precedence above: a__U31 U31 head U51 a__head a__U81(x1,x2,x3,x4) weight: max{0, (/ 288071 16) + x4, (/ 36009 2) + x3, (/ 36009 2) + x1} status: [] precedence above: a__U82 pair U61 a__U61 U81 U82 #a__take(x1,x2) weight: (/ 1 16) + x2 + x1 status: [x1,x2] precedence above: isNatural(x1) weight: 0 status: [] precedence above: U21 U11 isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head cons a__U61 snd U81 U82 tt a__isNatural U51 a__head a__U41(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 8) + x1} status: [x1] precedence above: cons tt U41 #a__U21(x1,x2) weight: x1 status: [x1] precedence above: #a__U81(x1,x2,x3,x4) weight: max{0, x2} status: [x2] precedence above: U21 U11 isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head #a__splitAt cons a__U61 snd U81 U82 tt a__isNatural U51 a__head #a__U61(x1,x2) weight: (/ 1 16) + x2 + x1 status: [x2,x1] precedence above: a__fst(x1) weight: (/ 1 8) + x1 status: [] precedence above: U21 U11 s isPLNat U91 a__U82 U71 pair fst a__snd splitAt a__U31 a__U51 a__U81 isNatural #a__U81 a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head #a__splitAt cons a__U61 snd U81 U82 tt a__isNatural U51 a__head tail(x1) weight: (/ 1 4) + x1 status: [] precedence above: U21 U11 s isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural #a__U81 a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head #a__splitAt cons a__U61 snd U81 U82 tt a__isNatural U51 a__tail a__head a__natsFrom(x1) weight: (/ 3 16) + x1 status: [] precedence above: natsFrom a__U41 cons tt U41 #mark(x1) weight: x1 status: [] precedence above: 0() weight: (/ 1 16) status: [] precedence above: tt #a__and(x1,x2) weight: max{0, (/ 1 16) + x2} status: [x2] precedence above: a__isLNat(x1) weight: 0 status: [] precedence above: U21 U11 isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head cons a__U61 snd U81 U82 tt a__isNatural U51 a__head a__U21(x1,x2) weight: max{0, (/ 288069 16) + x2} status: [] precedence above: U21 U11 isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural a__isLNat a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head cons a__U61 snd U81 U82 tt a__isNatural U51 a__head a__U91(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 8) + x1} status: [] precedence above: U21 U11 isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural a__isLNat a__U21 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head cons a__U61 snd U81 U82 tt a__isNatural U51 a__head sel(x1,x2) weight: 18005 + x2 + x1 status: [x1] precedence above: a__U31 a__U51 a__sel U31 head U51 a__head afterNth(x1,x2) weight: max{(/ 288073 16) + x2, (/ 288069 16) + x1} status: [x2,x1] precedence above: U11 a__afterNth a__U11 nil() weight: (/ 1 16) status: [] precedence above: tt a__splitAt(x1,x2) weight: max{0, (/ 288071 16) + x2} status: [] precedence above: a__U82 U71 pair splitAt a__U81 U61 a__U71 a__U61 U81 U82 isLNat(x1) weight: 0 status: [] precedence above: U21 U11 isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural a__isLNat a__U21 a__U91 sel a__splitAt mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head cons a__U61 snd U81 U82 tt a__isNatural U51 a__head #a__sel(x1,x2) weight: (/ 1 16) + x2 + x1 status: [x2,x1] precedence above: mark(x1) weight: x1 status: x1 #a__isLNat(x1) weight: (/ 1 16) status: [] precedence above: #a__U101(x1,x2,x3) weight: (/ 1 16) + x3 + x1 status: [x1,x3] precedence above: a__U11(x1,x2,x3) weight: max{(/ 36009 2) + x3, (/ 1 16) + x2, (/ 144035 8) + x1} status: [x1,x3] precedence above: U11 a__sel(x1,x2) weight: 18005 + x2 + x1 status: [x1] precedence above: a__U31 a__U51 sel U31 head U51 a__head a__isPLNat(x1) weight: 0 status: [] precedence above: U21 U11 isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel U61 U31 a__U71 head cons a__U61 snd U81 U82 tt a__isNatural U51 a__head U61(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} status: [x1] precedence above: a__U61 U31(x1,x2) weight: max{(/ 1 8) + x2, (/ 1 16) + x1} status: [] precedence above: a__U31 a__U71(x1,x2) weight: max{0, (/ 144035 8) + x2} status: [] precedence above: U71 pair U61 a__U61 #a__isPLNat(x1) weight: (/ 1 16) status: [] precedence above: head(x1) weight: (/ 3 16) + x1 status: [] precedence above: a__U31 U31 a__head #a__afterNth(x1,x2) weight: (/ 1 16) + x2 + x1 status: [x1,x2] precedence above: #a__splitAt(x1,x2) weight: max{0, x1} status: [x1] precedence above: cons(x1,x2) weight: max{x2, (/ 1 16) + x1} status: [x1] precedence above: tt a__U61(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} status: [x1] precedence above: U61 snd(x1) weight: x1 status: x1 a__take(x1,x2) weight: (/ 288073 16) + x2 status: [] precedence above: U21 U11 s isPLNat U91 a__U82 take U71 U101 pair fst a__snd splitAt a__U31 a__U51 a__U81 isNatural #a__U81 a__fst a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head #a__splitAt cons a__U61 snd U81 U82 tt a__isNatural U51 a__U101 a__head U81(x1,x2,x3,x4) weight: max{0, (/ 288071 16) + x4, (/ 36009 2) + x3, (/ 36009 2) + x1} status: [] precedence above: a__U82 pair a__U81 U61 a__U61 U82 #a__U41(x1,x2) weight: (/ 1 16) status: [] precedence above: U82(x1,x2) weight: max{(/ 36009 2) + x2, x1} status: [] precedence above: a__U82 pair U61 a__U61 tt() weight: 0 status: [] precedence above: a__isNatural(x1) weight: 0 status: [] precedence above: U21 U11 isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head cons a__U61 snd U81 U82 tt U51 a__head #a__isNatural(x1) weight: (/ 1 16) status: [] precedence above: #a__fst(x1) weight: x1 status: [] precedence above: U51(x1,x2,x3) weight: max{(/ 288079 16) + x3, (/ 144039 8) + x2, (/ 288077 16) + x1} status: [x2] precedence above: a__U31 a__U51 U31 head a__head a__and(x1,x2) weight: max{0, x2} status: x2 a__tail(x1) weight: (/ 1 4) + x1 status: [] precedence above: U21 U11 s isPLNat U91 a__U82 U71 pair a__snd splitAt a__U31 a__U51 a__U81 isNatural #a__U81 tail a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head #a__splitAt cons a__U61 snd U81 U82 tt a__isNatural U51 a__head U41(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 8) + x1} status: [x1] precedence above: a__U41 cons tt #a__tail(x1) weight: x1 status: [] precedence above: a__U101(x1,x2,x3) weight: max{0, (/ 288073 16) + x3} status: [] precedence above: U21 U11 s isPLNat U91 a__U82 U71 U101 pair fst a__snd splitAt a__U31 a__U51 a__U81 isNatural #a__U81 a__fst a__isLNat a__U21 a__U91 sel a__splitAt isLNat mark a__U11 a__sel a__isPLNat U61 U31 a__U71 head #a__splitAt cons a__U61 snd U81 U82 tt a__isNatural U51 a__head #a__U91(x1,x2) weight: x2 status: [x2] precedence above: a__head(x1) weight: (/ 3 16) + x1 status: [] precedence above: a__U31 U31 head Usable rules: { 1..90 } Removed DPs: #45 #89 Number of SCCs: 1, DPs: 26, edges: 119 SCC { #7 #8 #38 #43 #49..51 #60 #68 #71 #72 #86..88 #92 #93 #97 #98 #102..104 #108 #114 #115 #123 #124 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2) weight: (/ 1 16) + x1 #a__U82(x1,x2) weight: 0 #a__U71(x1,x2) weight: 0 U11(x1,x2,x3) weight: (/ 5 16) + x3 s(x1) weight: (/ 1 16) + x1 #a__U31(x1,x2) weight: 0 #a__head(x1) weight: 0 #a__natsFrom(x1) weight: 0 isPLNat(x1) weight: (/ 1 4) + x1 #a__snd(x1) weight: 0 a__afterNth(x1,x2) weight: x1 + x2 U91(x1,x2) weight: (/ 5 16) + x1 a__U82(x1,x2) weight: (/ 13 16) take(x1,x2) weight: (/ 3 16) + x1 + x2 U71(x1,x2) weight: (/ 1 4) and(x1,x2) weight: (/ 5 16) + x1 + x2 U101(x1,x2,x3) weight: (/ 7 16) + x1 + x2 pair(x1,x2) weight: (/ 1 16) + x1 + x2 fst(x1) weight: (/ 3 16) + x1 natsFrom(x1) weight: (/ 3 16) + x1 a__snd(x1) weight: x1 #a__U51(x1,x2,x3) weight: 0 splitAt(x1,x2) weight: (/ 1 16) + x1 + x2 #a__U11(x1,x2,x3) weight: 0 a__U31(x1,x2) weight: (/ 1 4) + x2 a__U51(x1,x2,x3) weight: (/ 1 8) + x1 + x2 + x3 a__U81(x1,x2,x3,x4) weight: (/ 3 4) + x2 #a__take(x1,x2) weight: 0 isNatural(x1) weight: (/ 1 4) + x1 a__U41(x1,x2) weight: (/ 5 8) + x2 #a__U21(x1,x2) weight: 0 #a__U81(x1,x2,x3,x4) weight: 0 #a__U61(x1,x2) weight: 0 a__fst(x1) weight: x1 tail(x1) weight: (/ 1 16) + x1 a__natsFrom(x1) weight: (/ 9 16) #mark(x1) weight: x1 0() weight: 0 #a__and(x1,x2) weight: (/ 1 16) + x2 a__isLNat(x1) weight: (/ 1 16) a__U21(x1,x2) weight: x1 a__U91(x1,x2) weight: (/ 1 4) sel(x1,x2) weight: (/ 1 16) + x1 + x2 afterNth(x1,x2) weight: (/ 3 16) + x1 + x2 nil() weight: 0 a__splitAt(x1,x2) weight: (/ 1 8) + x2 isLNat(x1) weight: (/ 1 8) + x1 #a__sel(x1,x2) weight: 0 mark(x1) weight: (/ 5 16) + x1 #a__isLNat(x1) weight: (/ 1 16) + x1 #a__U101(x1,x2,x3) weight: 0 a__U11(x1,x2,x3) weight: (/ 3 8) + x1 a__sel(x1,x2) weight: 0 a__isPLNat(x1) weight: (/ 1 8) + x1 U61(x1,x2) weight: (/ 1 16) + x2 U31(x1,x2) weight: (/ 5 16) + x1 a__U71(x1,x2) weight: (/ 3 16) #a__isPLNat(x1) weight: (/ 3 16) + x1 head(x1) weight: (/ 1 4) + x1 #a__afterNth(x1,x2) weight: 0 #a__splitAt(x1,x2) weight: 0 cons(x1,x2) weight: (/ 3 16) + x1 + x2 a__U61(x1,x2) weight: (/ 1 8) + x1 snd(x1) weight: (/ 3 16) + x1 a__take(x1,x2) weight: (/ 1 4) + x1 U81(x1,x2,x3,x4) weight: (/ 13 16) + x3 + x4 #a__U41(x1,x2) weight: 0 U82(x1,x2) weight: (/ 7 8) + x1 tt() weight: 0 a__isNatural(x1) weight: (/ 3 16) #a__isNatural(x1) weight: (/ 3 16) + x1 #a__fst(x1) weight: 0 U51(x1,x2,x3) weight: (/ 1 16) a__and(x1,x2) weight: (/ 1 4) a__tail(x1) weight: (/ 7 16) U41(x1,x2) weight: (/ 1 4) + x1 #a__tail(x1) weight: 0 a__U101(x1,x2,x3) weight: (/ 3 8) + x2 + x3 #a__U91(x1,x2) weight: 0 a__head(x1) weight: (/ 3 16) Usable rules: { } Removed DPs: #7 #8 #38 #43 #49..51 #60 #68 #71 #72 #86..88 #92 #93 #97 #98 #102..104 #108 #114 #115 #123 #124 Number of SCCs: 0, DPs: 0, edges: 0 YES