Input TRS: 1: a__U101(tt(),V1,V2) -> a__U102(a__isNaturalKind(V1),V1,V2) 2: a__U102(tt(),V1,V2) -> a__U103(a__isLNatKind(V2),V1,V2) 3: a__U103(tt(),V1,V2) -> a__U104(a__isLNatKind(V2),V1,V2) 4: a__U104(tt(),V1,V2) -> a__U105(a__isNatural(V1),V2) 5: a__U105(tt(),V2) -> a__U106(a__isLNat(V2)) 6: a__U106(tt()) -> tt() 7: a__U11(tt(),N,XS) -> a__U12(a__isNaturalKind(N),N,XS) 8: a__U111(tt(),V2) -> a__U112(a__isLNatKind(V2)) 9: a__U112(tt()) -> tt() 10: a__U12(tt(),N,XS) -> a__U13(a__isLNat(XS),N,XS) 11: a__U121(tt(),V2) -> a__U122(a__isLNatKind(V2)) 12: a__U122(tt()) -> tt() 13: a__U13(tt(),N,XS) -> a__U14(a__isLNatKind(XS),N,XS) 14: a__U131(tt()) -> tt() 15: a__U14(tt(),N,XS) -> a__snd(a__splitAt(mark(N),mark(XS))) 16: a__U141(tt()) -> tt() 17: a__U151(tt()) -> tt() 18: a__U161(tt()) -> tt() 19: a__U171(tt(),V2) -> a__U172(a__isLNatKind(V2)) 20: a__U172(tt()) -> tt() 21: a__U181(tt(),V1) -> a__U182(a__isLNatKind(V1),V1) 22: a__U182(tt(),V1) -> a__U183(a__isLNat(V1)) 23: a__U183(tt()) -> tt() 24: a__U191(tt(),V1) -> a__U192(a__isNaturalKind(V1),V1) 25: a__U192(tt(),V1) -> a__U193(a__isNatural(V1)) 26: a__U193(tt()) -> tt() 27: a__U201(tt(),V1,V2) -> a__U202(a__isNaturalKind(V1),V1,V2) 28: a__U202(tt(),V1,V2) -> a__U203(a__isLNatKind(V2),V1,V2) 29: a__U203(tt(),V1,V2) -> a__U204(a__isLNatKind(V2),V1,V2) 30: a__U204(tt(),V1,V2) -> a__U205(a__isNatural(V1),V2) 31: a__U205(tt(),V2) -> a__U206(a__isLNat(V2)) 32: a__U206(tt()) -> tt() 33: a__U21(tt(),X,Y) -> a__U22(a__isLNatKind(X),X,Y) 34: a__U211(tt()) -> tt() 35: a__U22(tt(),X,Y) -> a__U23(a__isLNat(Y),X,Y) 36: a__U221(tt()) -> tt() 37: a__U23(tt(),X,Y) -> a__U24(a__isLNatKind(Y),X) 38: a__U231(tt(),V2) -> a__U232(a__isLNatKind(V2)) 39: a__U232(tt()) -> tt() 40: a__U24(tt(),X) -> mark(X) 41: a__U241(tt(),V1,V2) -> a__U242(a__isLNatKind(V1),V1,V2) 42: a__U242(tt(),V1,V2) -> a__U243(a__isLNatKind(V2),V1,V2) 43: a__U243(tt(),V1,V2) -> a__U244(a__isLNatKind(V2),V1,V2) 44: a__U244(tt(),V1,V2) -> a__U245(a__isLNat(V1),V2) 45: a__U245(tt(),V2) -> a__U246(a__isLNat(V2)) 46: a__U246(tt()) -> tt() 47: a__U251(tt(),V1,V2) -> a__U252(a__isNaturalKind(V1),V1,V2) 48: a__U252(tt(),V1,V2) -> a__U253(a__isLNatKind(V2),V1,V2) 49: a__U253(tt(),V1,V2) -> a__U254(a__isLNatKind(V2),V1,V2) 50: a__U254(tt(),V1,V2) -> a__U255(a__isNatural(V1),V2) 51: a__U255(tt(),V2) -> a__U256(a__isLNat(V2)) 52: a__U256(tt()) -> tt() 53: a__U261(tt(),V2) -> a__U262(a__isLNatKind(V2)) 54: a__U262(tt()) -> tt() 55: a__U271(tt(),V2) -> a__U272(a__isLNatKind(V2)) 56: a__U272(tt()) -> tt() 57: a__U281(tt(),N) -> a__U282(a__isNaturalKind(N),N) 58: a__U282(tt(),N) -> cons(mark(N),natsFrom(s(N))) 59: a__U291(tt(),N,XS) -> a__U292(a__isNaturalKind(N),N,XS) 60: a__U292(tt(),N,XS) -> a__U293(a__isLNat(XS),N,XS) 61: a__U293(tt(),N,XS) -> a__U294(a__isLNatKind(XS),N,XS) 62: a__U294(tt(),N,XS) -> a__head(a__afterNth(mark(N),mark(XS))) 63: a__U301(tt(),X,Y) -> a__U302(a__isLNatKind(X),Y) 64: a__U302(tt(),Y) -> a__U303(a__isLNat(Y),Y) 65: a__U303(tt(),Y) -> a__U304(a__isLNatKind(Y),Y) 66: a__U304(tt(),Y) -> mark(Y) 67: a__U31(tt(),N,XS) -> a__U32(a__isNaturalKind(N),N,XS) 68: a__U311(tt(),XS) -> a__U312(a__isLNatKind(XS),XS) 69: a__U312(tt(),XS) -> pair(nil(),mark(XS)) 70: a__U32(tt(),N,XS) -> a__U33(a__isLNat(XS),N,XS) 71: a__U321(tt(),N,X,XS) -> a__U322(a__isNaturalKind(N),N,X,XS) 72: a__U322(tt(),N,X,XS) -> a__U323(a__isNatural(X),N,X,XS) 73: a__U323(tt(),N,X,XS) -> a__U324(a__isNaturalKind(X),N,X,XS) 74: a__U324(tt(),N,X,XS) -> a__U325(a__isLNat(XS),N,X,XS) 75: a__U325(tt(),N,X,XS) -> a__U326(a__isLNatKind(XS),N,X,XS) 76: a__U326(tt(),N,X,XS) -> a__U327(a__splitAt(mark(N),mark(XS)),X) 77: a__U327(pair(YS,ZS),X) -> pair(cons(mark(X),YS),mark(ZS)) 78: a__U33(tt(),N,XS) -> a__U34(a__isLNatKind(XS),N) 79: a__U331(tt(),N,XS) -> a__U332(a__isNaturalKind(N),XS) 80: a__U332(tt(),XS) -> a__U333(a__isLNat(XS),XS) 81: a__U333(tt(),XS) -> a__U334(a__isLNatKind(XS),XS) 82: a__U334(tt(),XS) -> mark(XS) 83: a__U34(tt(),N) -> mark(N) 84: a__U341(tt(),N,XS) -> a__U342(a__isNaturalKind(N),N,XS) 85: a__U342(tt(),N,XS) -> a__U343(a__isLNat(XS),N,XS) 86: a__U343(tt(),N,XS) -> a__U344(a__isLNatKind(XS),N,XS) 87: a__U344(tt(),N,XS) -> a__fst(a__splitAt(mark(N),mark(XS))) 88: a__U41(tt(),V1,V2) -> a__U42(a__isNaturalKind(V1),V1,V2) 89: a__U42(tt(),V1,V2) -> a__U43(a__isLNatKind(V2),V1,V2) 90: a__U43(tt(),V1,V2) -> a__U44(a__isLNatKind(V2),V1,V2) 91: a__U44(tt(),V1,V2) -> a__U45(a__isNatural(V1),V2) 92: a__U45(tt(),V2) -> a__U46(a__isLNat(V2)) 93: a__U46(tt()) -> tt() 94: a__U51(tt(),V1,V2) -> a__U52(a__isNaturalKind(V1),V1,V2) 95: a__U52(tt(),V1,V2) -> a__U53(a__isLNatKind(V2),V1,V2) 96: a__U53(tt(),V1,V2) -> a__U54(a__isLNatKind(V2),V1,V2) 97: a__U54(tt(),V1,V2) -> a__U55(a__isNatural(V1),V2) 98: a__U55(tt(),V2) -> a__U56(a__isLNat(V2)) 99: a__U56(tt()) -> tt() 100: a__U61(tt(),V1) -> a__U62(a__isPLNatKind(V1),V1) 101: a__U62(tt(),V1) -> a__U63(a__isPLNat(V1)) 102: a__U63(tt()) -> tt() 103: a__U71(tt(),V1) -> a__U72(a__isNaturalKind(V1),V1) 104: a__U72(tt(),V1) -> a__U73(a__isNatural(V1)) 105: a__U73(tt()) -> tt() 106: a__U81(tt(),V1) -> a__U82(a__isPLNatKind(V1),V1) 107: a__U82(tt(),V1) -> a__U83(a__isPLNat(V1)) 108: a__U83(tt()) -> tt() 109: a__U91(tt(),V1) -> a__U92(a__isLNatKind(V1),V1) 110: a__U92(tt(),V1) -> a__U93(a__isLNat(V1)) 111: a__U93(tt()) -> tt() 112: a__afterNth(N,XS) -> a__U11(a__isNatural(N),N,XS) 113: a__fst(pair(X,Y)) -> a__U21(a__isLNat(X),X,Y) 114: a__head(cons(N,XS)) -> a__U31(a__isNatural(N),N,XS) 115: a__isLNat(nil()) -> tt() 116: a__isLNat(afterNth(V1,V2)) -> a__U41(a__isNaturalKind(V1),V1,V2) 117: a__isLNat(cons(V1,V2)) -> a__U51(a__isNaturalKind(V1),V1,V2) 118: a__isLNat(fst(V1)) -> a__U61(a__isPLNatKind(V1),V1) 119: a__isLNat(natsFrom(V1)) -> a__U71(a__isNaturalKind(V1),V1) 120: a__isLNat(snd(V1)) -> a__U81(a__isPLNatKind(V1),V1) 121: a__isLNat(tail(V1)) -> a__U91(a__isLNatKind(V1),V1) 122: a__isLNat(take(V1,V2)) -> a__U101(a__isNaturalKind(V1),V1,V2) 123: a__isLNatKind(nil()) -> tt() 124: a__isLNatKind(afterNth(V1,V2)) -> a__U111(a__isNaturalKind(V1),V2) 125: a__isLNatKind(cons(V1,V2)) -> a__U121(a__isNaturalKind(V1),V2) 126: a__isLNatKind(fst(V1)) -> a__U131(a__isPLNatKind(V1)) 127: a__isLNatKind(natsFrom(V1)) -> a__U141(a__isNaturalKind(V1)) 128: a__isLNatKind(snd(V1)) -> a__U151(a__isPLNatKind(V1)) 129: a__isLNatKind(tail(V1)) -> a__U161(a__isLNatKind(V1)) 130: a__isLNatKind(take(V1,V2)) -> a__U171(a__isNaturalKind(V1),V2) 131: a__isNatural(0()) -> tt() 132: a__isNatural(head(V1)) -> a__U181(a__isLNatKind(V1),V1) 133: a__isNatural(s(V1)) -> a__U191(a__isNaturalKind(V1),V1) 134: a__isNatural(sel(V1,V2)) -> a__U201(a__isNaturalKind(V1),V1,V2) 135: a__isNaturalKind(0()) -> tt() 136: a__isNaturalKind(head(V1)) -> a__U211(a__isLNatKind(V1)) 137: a__isNaturalKind(s(V1)) -> a__U221(a__isNaturalKind(V1)) 138: a__isNaturalKind(sel(V1,V2)) -> a__U231(a__isNaturalKind(V1),V2) 139: a__isPLNat(pair(V1,V2)) -> a__U241(a__isLNatKind(V1),V1,V2) 140: a__isPLNat(splitAt(V1,V2)) -> a__U251(a__isNaturalKind(V1),V1,V2) 141: a__isPLNatKind(pair(V1,V2)) -> a__U261(a__isLNatKind(V1),V2) 142: a__isPLNatKind(splitAt(V1,V2)) -> a__U271(a__isNaturalKind(V1),V2) 143: a__natsFrom(N) -> a__U281(a__isNatural(N),N) 144: a__sel(N,XS) -> a__U291(a__isNatural(N),N,XS) 145: a__snd(pair(X,Y)) -> a__U301(a__isLNat(X),X,Y) 146: a__splitAt(0(),XS) -> a__U311(a__isLNat(XS),XS) 147: a__splitAt(s(N),cons(X,XS)) -> a__U321(a__isNatural(N),N,X,XS) 148: a__tail(cons(N,XS)) -> a__U331(a__isNatural(N),N,XS) 149: a__take(N,XS) -> a__U341(a__isNatural(N),N,XS) 150: mark(U101(X1,X2,X3)) -> a__U101(mark(X1),X2,X3) 151: mark(U102(X1,X2,X3)) -> a__U102(mark(X1),X2,X3) 152: mark(isNaturalKind(X)) -> a__isNaturalKind(X) 153: mark(U103(X1,X2,X3)) -> a__U103(mark(X1),X2,X3) 154: mark(isLNatKind(X)) -> a__isLNatKind(X) 155: mark(U104(X1,X2,X3)) -> a__U104(mark(X1),X2,X3) 156: mark(U105(X1,X2)) -> a__U105(mark(X1),X2) 157: mark(isNatural(X)) -> a__isNatural(X) 158: mark(U106(X)) -> a__U106(mark(X)) 159: mark(isLNat(X)) -> a__isLNat(X) 160: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3) 161: mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3) 162: mark(U111(X1,X2)) -> a__U111(mark(X1),X2) 163: mark(U112(X)) -> a__U112(mark(X)) 164: mark(U13(X1,X2,X3)) -> a__U13(mark(X1),X2,X3) 165: mark(U121(X1,X2)) -> a__U121(mark(X1),X2) 166: mark(U122(X)) -> a__U122(mark(X)) 167: mark(U14(X1,X2,X3)) -> a__U14(mark(X1),X2,X3) 168: mark(U131(X)) -> a__U131(mark(X)) 169: mark(snd(X)) -> a__snd(mark(X)) 170: mark(splitAt(X1,X2)) -> a__splitAt(mark(X1),mark(X2)) 171: mark(U141(X)) -> a__U141(mark(X)) 172: mark(U151(X)) -> a__U151(mark(X)) 173: mark(U161(X)) -> a__U161(mark(X)) 174: mark(U171(X1,X2)) -> a__U171(mark(X1),X2) 175: mark(U172(X)) -> a__U172(mark(X)) 176: mark(U181(X1,X2)) -> a__U181(mark(X1),X2) 177: mark(U182(X1,X2)) -> a__U182(mark(X1),X2) 178: mark(U183(X)) -> a__U183(mark(X)) 179: mark(U191(X1,X2)) -> a__U191(mark(X1),X2) 180: mark(U192(X1,X2)) -> a__U192(mark(X1),X2) 181: mark(U193(X)) -> a__U193(mark(X)) 182: mark(U201(X1,X2,X3)) -> a__U201(mark(X1),X2,X3) 183: mark(U202(X1,X2,X3)) -> a__U202(mark(X1),X2,X3) 184: mark(U203(X1,X2,X3)) -> a__U203(mark(X1),X2,X3) 185: mark(U204(X1,X2,X3)) -> a__U204(mark(X1),X2,X3) 186: mark(U205(X1,X2)) -> a__U205(mark(X1),X2) 187: mark(U206(X)) -> a__U206(mark(X)) 188: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3) 189: mark(U22(X1,X2,X3)) -> a__U22(mark(X1),X2,X3) 190: mark(U211(X)) -> a__U211(mark(X)) 191: mark(U23(X1,X2,X3)) -> a__U23(mark(X1),X2,X3) 192: mark(U221(X)) -> a__U221(mark(X)) 193: mark(U24(X1,X2)) -> a__U24(mark(X1),X2) 194: mark(U231(X1,X2)) -> a__U231(mark(X1),X2) 195: mark(U232(X)) -> a__U232(mark(X)) 196: mark(U241(X1,X2,X3)) -> a__U241(mark(X1),X2,X3) 197: mark(U242(X1,X2,X3)) -> a__U242(mark(X1),X2,X3) 198: mark(U243(X1,X2,X3)) -> a__U243(mark(X1),X2,X3) 199: mark(U244(X1,X2,X3)) -> a__U244(mark(X1),X2,X3) 200: mark(U245(X1,X2)) -> a__U245(mark(X1),X2) 201: mark(U246(X)) -> a__U246(mark(X)) 202: mark(U251(X1,X2,X3)) -> a__U251(mark(X1),X2,X3) 203: mark(U252(X1,X2,X3)) -> a__U252(mark(X1),X2,X3) 204: mark(U253(X1,X2,X3)) -> a__U253(mark(X1),X2,X3) 205: mark(U254(X1,X2,X3)) -> a__U254(mark(X1),X2,X3) 206: mark(U255(X1,X2)) -> a__U255(mark(X1),X2) 207: mark(U256(X)) -> a__U256(mark(X)) 208: mark(U261(X1,X2)) -> a__U261(mark(X1),X2) 209: mark(U262(X)) -> a__U262(mark(X)) 210: mark(U271(X1,X2)) -> a__U271(mark(X1),X2) 211: mark(U272(X)) -> a__U272(mark(X)) 212: mark(U281(X1,X2)) -> a__U281(mark(X1),X2) 213: mark(U282(X1,X2)) -> a__U282(mark(X1),X2) 214: mark(natsFrom(X)) -> a__natsFrom(mark(X)) 215: mark(U291(X1,X2,X3)) -> a__U291(mark(X1),X2,X3) 216: mark(U292(X1,X2,X3)) -> a__U292(mark(X1),X2,X3) 217: mark(U293(X1,X2,X3)) -> a__U293(mark(X1),X2,X3) 218: mark(U294(X1,X2,X3)) -> a__U294(mark(X1),X2,X3) 219: mark(head(X)) -> a__head(mark(X)) 220: mark(afterNth(X1,X2)) -> a__afterNth(mark(X1),mark(X2)) 221: mark(U301(X1,X2,X3)) -> a__U301(mark(X1),X2,X3) 222: mark(U302(X1,X2)) -> a__U302(mark(X1),X2) 223: mark(U303(X1,X2)) -> a__U303(mark(X1),X2) 224: mark(U304(X1,X2)) -> a__U304(mark(X1),X2) 225: mark(U31(X1,X2,X3)) -> a__U31(mark(X1),X2,X3) 226: mark(U32(X1,X2,X3)) -> a__U32(mark(X1),X2,X3) 227: mark(U311(X1,X2)) -> a__U311(mark(X1),X2) 228: mark(U312(X1,X2)) -> a__U312(mark(X1),X2) 229: mark(U33(X1,X2,X3)) -> a__U33(mark(X1),X2,X3) 230: mark(U321(X1,X2,X3,X4)) -> a__U321(mark(X1),X2,X3,X4) 231: mark(U322(X1,X2,X3,X4)) -> a__U322(mark(X1),X2,X3,X4) 232: mark(U323(X1,X2,X3,X4)) -> a__U323(mark(X1),X2,X3,X4) 233: mark(U324(X1,X2,X3,X4)) -> a__U324(mark(X1),X2,X3,X4) 234: mark(U325(X1,X2,X3,X4)) -> a__U325(mark(X1),X2,X3,X4) 235: mark(U326(X1,X2,X3,X4)) -> a__U326(mark(X1),X2,X3,X4) 236: mark(U327(X1,X2)) -> a__U327(mark(X1),X2) 237: mark(U34(X1,X2)) -> a__U34(mark(X1),X2) 238: mark(U331(X1,X2,X3)) -> a__U331(mark(X1),X2,X3) 239: mark(U332(X1,X2)) -> a__U332(mark(X1),X2) 240: mark(U333(X1,X2)) -> a__U333(mark(X1),X2) 241: mark(U334(X1,X2)) -> a__U334(mark(X1),X2) 242: mark(U341(X1,X2,X3)) -> a__U341(mark(X1),X2,X3) 243: mark(U342(X1,X2,X3)) -> a__U342(mark(X1),X2,X3) 244: mark(U343(X1,X2,X3)) -> a__U343(mark(X1),X2,X3) 245: mark(U344(X1,X2,X3)) -> a__U344(mark(X1),X2,X3) 246: mark(fst(X)) -> a__fst(mark(X)) 247: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3) 248: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3) 249: mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3) 250: mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3) 251: mark(U45(X1,X2)) -> a__U45(mark(X1),X2) 252: mark(U46(X)) -> a__U46(mark(X)) 253: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3) 254: mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3) 255: mark(U53(X1,X2,X3)) -> a__U53(mark(X1),X2,X3) 256: mark(U54(X1,X2,X3)) -> a__U54(mark(X1),X2,X3) 257: mark(U55(X1,X2)) -> a__U55(mark(X1),X2) 258: mark(U56(X)) -> a__U56(mark(X)) 259: mark(U61(X1,X2)) -> a__U61(mark(X1),X2) 260: mark(U62(X1,X2)) -> a__U62(mark(X1),X2) 261: mark(isPLNatKind(X)) -> a__isPLNatKind(X) 262: mark(U63(X)) -> a__U63(mark(X)) 263: mark(isPLNat(X)) -> a__isPLNat(X) 264: mark(U71(X1,X2)) -> a__U71(mark(X1),X2) 265: mark(U72(X1,X2)) -> a__U72(mark(X1),X2) 266: mark(U73(X)) -> a__U73(mark(X)) 267: mark(U81(X1,X2)) -> a__U81(mark(X1),X2) 268: mark(U82(X1,X2)) -> a__U82(mark(X1),X2) 269: mark(U83(X)) -> a__U83(mark(X)) 270: mark(U91(X1,X2)) -> a__U91(mark(X1),X2) 271: mark(U92(X1,X2)) -> a__U92(mark(X1),X2) 272: mark(U93(X)) -> a__U93(mark(X)) 273: mark(tail(X)) -> a__tail(mark(X)) 274: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) 275: mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) 276: mark(tt()) -> tt() 277: mark(cons(X1,X2)) -> cons(mark(X1),X2) 278: mark(s(X)) -> s(mark(X)) 279: mark(pair(X1,X2)) -> pair(mark(X1),mark(X2)) 280: mark(nil()) -> nil() 281: mark(0()) -> 0() 282: a__U101(X1,X2,X3) -> U101(X1,X2,X3) 283: a__U102(X1,X2,X3) -> U102(X1,X2,X3) 284: a__isNaturalKind(X) -> isNaturalKind(X) 285: a__U103(X1,X2,X3) -> U103(X1,X2,X3) 286: a__isLNatKind(X) -> isLNatKind(X) 287: a__U104(X1,X2,X3) -> U104(X1,X2,X3) 288: a__U105(X1,X2) -> U105(X1,X2) 289: a__isNatural(X) -> isNatural(X) 290: a__U106(X) -> U106(X) 291: a__isLNat(X) -> isLNat(X) 292: a__U11(X1,X2,X3) -> U11(X1,X2,X3) 293: a__U12(X1,X2,X3) -> U12(X1,X2,X3) 294: a__U111(X1,X2) -> U111(X1,X2) 295: a__U112(X) -> U112(X) 296: a__U13(X1,X2,X3) -> U13(X1,X2,X3) 297: a__U121(X1,X2) -> U121(X1,X2) 298: a__U122(X) -> U122(X) 299: a__U14(X1,X2,X3) -> U14(X1,X2,X3) 300: a__U131(X) -> U131(X) 301: a__snd(X) -> snd(X) 302: a__splitAt(X1,X2) -> splitAt(X1,X2) 303: a__U141(X) -> U141(X) 304: a__U151(X) -> U151(X) 305: a__U161(X) -> U161(X) 306: a__U171(X1,X2) -> U171(X1,X2) 307: a__U172(X) -> U172(X) 308: a__U181(X1,X2) -> U181(X1,X2) 309: a__U182(X1,X2) -> U182(X1,X2) 310: a__U183(X) -> U183(X) 311: a__U191(X1,X2) -> U191(X1,X2) 312: a__U192(X1,X2) -> U192(X1,X2) 313: a__U193(X) -> U193(X) 314: a__U201(X1,X2,X3) -> U201(X1,X2,X3) 315: a__U202(X1,X2,X3) -> U202(X1,X2,X3) 316: a__U203(X1,X2,X3) -> U203(X1,X2,X3) 317: a__U204(X1,X2,X3) -> U204(X1,X2,X3) 318: a__U205(X1,X2) -> U205(X1,X2) 319: a__U206(X) -> U206(X) 320: a__U21(X1,X2,X3) -> U21(X1,X2,X3) 321: a__U22(X1,X2,X3) -> U22(X1,X2,X3) 322: a__U211(X) -> U211(X) 323: a__U23(X1,X2,X3) -> U23(X1,X2,X3) 324: a__U221(X) -> U221(X) 325: a__U24(X1,X2) -> U24(X1,X2) 326: a__U231(X1,X2) -> U231(X1,X2) 327: a__U232(X) -> U232(X) 328: a__U241(X1,X2,X3) -> U241(X1,X2,X3) 329: a__U242(X1,X2,X3) -> U242(X1,X2,X3) 330: a__U243(X1,X2,X3) -> U243(X1,X2,X3) 331: a__U244(X1,X2,X3) -> U244(X1,X2,X3) 332: a__U245(X1,X2) -> U245(X1,X2) 333: a__U246(X) -> U246(X) 334: a__U251(X1,X2,X3) -> U251(X1,X2,X3) 335: a__U252(X1,X2,X3) -> U252(X1,X2,X3) 336: a__U253(X1,X2,X3) -> U253(X1,X2,X3) 337: a__U254(X1,X2,X3) -> U254(X1,X2,X3) 338: a__U255(X1,X2) -> U255(X1,X2) 339: a__U256(X) -> U256(X) 340: a__U261(X1,X2) -> U261(X1,X2) 341: a__U262(X) -> U262(X) 342: a__U271(X1,X2) -> U271(X1,X2) 343: a__U272(X) -> U272(X) 344: a__U281(X1,X2) -> U281(X1,X2) 345: a__U282(X1,X2) -> U282(X1,X2) 346: a__natsFrom(X) -> natsFrom(X) 347: a__U291(X1,X2,X3) -> U291(X1,X2,X3) 348: a__U292(X1,X2,X3) -> U292(X1,X2,X3) 349: a__U293(X1,X2,X3) -> U293(X1,X2,X3) 350: a__U294(X1,X2,X3) -> U294(X1,X2,X3) 351: a__head(X) -> head(X) 352: a__afterNth(X1,X2) -> afterNth(X1,X2) 353: a__U301(X1,X2,X3) -> U301(X1,X2,X3) 354: a__U302(X1,X2) -> U302(X1,X2) 355: a__U303(X1,X2) -> U303(X1,X2) 356: a__U304(X1,X2) -> U304(X1,X2) 357: a__U31(X1,X2,X3) -> U31(X1,X2,X3) 358: a__U32(X1,X2,X3) -> U32(X1,X2,X3) 359: a__U311(X1,X2) -> U311(X1,X2) 360: a__U312(X1,X2) -> U312(X1,X2) 361: a__U33(X1,X2,X3) -> U33(X1,X2,X3) 362: a__U321(X1,X2,X3,X4) -> U321(X1,X2,X3,X4) 363: a__U322(X1,X2,X3,X4) -> U322(X1,X2,X3,X4) 364: a__U323(X1,X2,X3,X4) -> U323(X1,X2,X3,X4) 365: a__U324(X1,X2,X3,X4) -> U324(X1,X2,X3,X4) 366: a__U325(X1,X2,X3,X4) -> U325(X1,X2,X3,X4) 367: a__U326(X1,X2,X3,X4) -> U326(X1,X2,X3,X4) 368: a__U327(X1,X2) -> U327(X1,X2) 369: a__U34(X1,X2) -> U34(X1,X2) 370: a__U331(X1,X2,X3) -> U331(X1,X2,X3) 371: a__U332(X1,X2) -> U332(X1,X2) 372: a__U333(X1,X2) -> U333(X1,X2) 373: a__U334(X1,X2) -> U334(X1,X2) 374: a__U341(X1,X2,X3) -> U341(X1,X2,X3) 375: a__U342(X1,X2,X3) -> U342(X1,X2,X3) 376: a__U343(X1,X2,X3) -> U343(X1,X2,X3) 377: a__U344(X1,X2,X3) -> U344(X1,X2,X3) 378: a__fst(X) -> fst(X) 379: a__U41(X1,X2,X3) -> U41(X1,X2,X3) 380: a__U42(X1,X2,X3) -> U42(X1,X2,X3) 381: a__U43(X1,X2,X3) -> U43(X1,X2,X3) 382: a__U44(X1,X2,X3) -> U44(X1,X2,X3) 383: a__U45(X1,X2) -> U45(X1,X2) 384: a__U46(X) -> U46(X) 385: a__U51(X1,X2,X3) -> U51(X1,X2,X3) 386: a__U52(X1,X2,X3) -> U52(X1,X2,X3) 387: a__U53(X1,X2,X3) -> U53(X1,X2,X3) 388: a__U54(X1,X2,X3) -> U54(X1,X2,X3) 389: a__U55(X1,X2) -> U55(X1,X2) 390: a__U56(X) -> U56(X) 391: a__U61(X1,X2) -> U61(X1,X2) 392: a__U62(X1,X2) -> U62(X1,X2) 393: a__isPLNatKind(X) -> isPLNatKind(X) 394: a__U63(X) -> U63(X) 395: a__isPLNat(X) -> isPLNat(X) 396: a__U71(X1,X2) -> U71(X1,X2) 397: a__U72(X1,X2) -> U72(X1,X2) 398: a__U73(X) -> U73(X) 399: a__U81(X1,X2) -> U81(X1,X2) 400: a__U82(X1,X2) -> U82(X1,X2) 401: a__U83(X) -> U83(X) 402: a__U91(X1,X2) -> U91(X1,X2) 403: a__U92(X1,X2) -> U92(X1,X2) 404: a__U93(X) -> U93(X) 405: a__tail(X) -> tail(X) 406: a__take(X1,X2) -> take(X1,X2) 407: a__sel(X1,X2) -> sel(X1,X2) Number of strict rules: 407 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #a__U102(tt(),V1,V2) -> #a__U103(a__isLNatKind(V2),V1,V2) #2: #a__U102(tt(),V1,V2) -> #a__isLNatKind(V2) #3: #a__U343(tt(),N,XS) -> #a__U344(a__isLNatKind(XS),N,XS) #4: #a__U343(tt(),N,XS) -> #a__isLNatKind(XS) #5: #a__U243(tt(),V1,V2) -> #a__U244(a__isLNatKind(V2),V1,V2) #6: #a__U243(tt(),V1,V2) -> #a__isLNatKind(V2) #7: #a__U203(tt(),V1,V2) -> #a__U204(a__isLNatKind(V2),V1,V2) #8: #a__U203(tt(),V1,V2) -> #a__isLNatKind(V2) #9: #mark(U331(X1,X2,X3)) -> #a__U331(mark(X1),X2,X3) #10: #mark(U331(X1,X2,X3)) -> #mark(X1) #11: #mark(isPLNat(X)) -> #a__isPLNat(X) #12: #a__U22(tt(),X,Y) -> #a__U23(a__isLNat(Y),X,Y) #13: #a__U22(tt(),X,Y) -> #a__isLNat(Y) #14: #a__U34(tt(),N) -> #mark(N) #15: #a__U304(tt(),Y) -> #mark(Y) #16: #mark(U182(X1,X2)) -> #a__U182(mark(X1),X2) #17: #mark(U182(X1,X2)) -> #mark(X1) #18: #mark(U33(X1,X2,X3)) -> #a__U33(mark(X1),X2,X3) #19: #mark(U33(X1,X2,X3)) -> #mark(X1) #20: #mark(U51(X1,X2,X3)) -> #a__U51(mark(X1),X2,X3) #21: #mark(U51(X1,X2,X3)) -> #mark(X1) #22: #a__U242(tt(),V1,V2) -> #a__U243(a__isLNatKind(V2),V1,V2) #23: #a__U242(tt(),V1,V2) -> #a__isLNatKind(V2) #24: #mark(U323(X1,X2,X3,X4)) -> #a__U323(mark(X1),X2,X3,X4) #25: #mark(U323(X1,X2,X3,X4)) -> #mark(X1) #26: #mark(U243(X1,X2,X3)) -> #a__U243(mark(X1),X2,X3) #27: #mark(U243(X1,X2,X3)) -> #mark(X1) #28: #a__take(N,XS) -> #a__U341(a__isNatural(N),N,XS) #29: #a__take(N,XS) -> #a__isNatural(N) #30: #a__U52(tt(),V1,V2) -> #a__U53(a__isLNatKind(V2),V1,V2) #31: #a__U52(tt(),V1,V2) -> #a__isLNatKind(V2) #32: #a__U241(tt(),V1,V2) -> #a__U242(a__isLNatKind(V1),V1,V2) #33: #a__U241(tt(),V1,V2) -> #a__isLNatKind(V1) #34: #mark(U42(X1,X2,X3)) -> #a__U42(mark(X1),X2,X3) #35: #mark(U42(X1,X2,X3)) -> #mark(X1) #36: #mark(U72(X1,X2)) -> #a__U72(mark(X1),X2) #37: #mark(U72(X1,X2)) -> #mark(X1) #38: #mark(U46(X)) -> #a__U46(mark(X)) #39: #mark(U46(X)) -> #mark(X) #40: #a__U23(tt(),X,Y) -> #a__U24(a__isLNatKind(Y),X) #41: #a__U23(tt(),X,Y) -> #a__isLNatKind(Y) #42: #a__head(cons(N,XS)) -> #a__U31(a__isNatural(N),N,XS) #43: #a__head(cons(N,XS)) -> #a__isNatural(N) #44: #mark(U321(X1,X2,X3,X4)) -> #a__U321(mark(X1),X2,X3,X4) #45: #mark(U321(X1,X2,X3,X4)) -> #mark(X1) #46: #mark(U112(X)) -> #a__U112(mark(X)) #47: #mark(U112(X)) -> #mark(X) #48: #a__U54(tt(),V1,V2) -> #a__U55(a__isNatural(V1),V2) #49: #a__U54(tt(),V1,V2) -> #a__isNatural(V1) #50: #a__U44(tt(),V1,V2) -> #a__U45(a__isNatural(V1),V2) #51: #a__U44(tt(),V1,V2) -> #a__isNatural(V1) #52: #a__U323(tt(),N,X,XS) -> #a__U324(a__isNaturalKind(X),N,X,XS) #53: #a__U323(tt(),N,X,XS) -> #a__isNaturalKind(X) #54: #a__U251(tt(),V1,V2) -> #a__U252(a__isNaturalKind(V1),V1,V2) #55: #a__U251(tt(),V1,V2) -> #a__isNaturalKind(V1) #56: #mark(U294(X1,X2,X3)) -> #a__U294(mark(X1),X2,X3) #57: #mark(U294(X1,X2,X3)) -> #mark(X1) #58: #mark(U23(X1,X2,X3)) -> #a__U23(mark(X1),X2,X3) #59: #mark(U23(X1,X2,X3)) -> #mark(X1) #60: #mark(U333(X1,X2)) -> #a__U333(mark(X1),X2) #61: #mark(U333(X1,X2)) -> #mark(X1) #62: #a__U261(tt(),V2) -> #a__U262(a__isLNatKind(V2)) #63: #a__U261(tt(),V2) -> #a__isLNatKind(V2) #64: #mark(U62(X1,X2)) -> #a__U62(mark(X1),X2) #65: #mark(U62(X1,X2)) -> #mark(X1) #66: #mark(U161(X)) -> #a__U161(mark(X)) #67: #mark(U161(X)) -> #mark(X) #68: #mark(U325(X1,X2,X3,X4)) -> #a__U325(mark(X1),X2,X3,X4) #69: #mark(U325(X1,X2,X3,X4)) -> #mark(X1) #70: #a__U321(tt(),N,X,XS) -> #a__U322(a__isNaturalKind(N),N,X,XS) #71: #a__U321(tt(),N,X,XS) -> #a__isNaturalKind(N) #72: #a__splitAt(s(N),cons(X,XS)) -> #a__U321(a__isNatural(N),N,X,XS) #73: #a__splitAt(s(N),cons(X,XS)) -> #a__isNatural(N) #74: #a__isPLNat(pair(V1,V2)) -> #a__U241(a__isLNatKind(V1),V1,V2) #75: #a__isPLNat(pair(V1,V2)) -> #a__isLNatKind(V1) #76: #a__U252(tt(),V1,V2) -> #a__U253(a__isLNatKind(V2),V1,V2) #77: #a__U252(tt(),V1,V2) -> #a__isLNatKind(V2) #78: #mark(U81(X1,X2)) -> #a__U81(mark(X1),X2) #79: #mark(U81(X1,X2)) -> #mark(X1) #80: #a__U325(tt(),N,X,XS) -> #a__U326(a__isLNatKind(XS),N,X,XS) #81: #a__U325(tt(),N,X,XS) -> #a__isLNatKind(XS) #82: #mark(U53(X1,X2,X3)) -> #a__U53(mark(X1),X2,X3) #83: #mark(U53(X1,X2,X3)) -> #mark(X1) #84: #mark(U183(X)) -> #a__U183(mark(X)) #85: #mark(U183(X)) -> #mark(X) #86: #a__afterNth(N,XS) -> #a__U11(a__isNatural(N),N,XS) #87: #a__afterNth(N,XS) -> #a__isNatural(N) #88: #a__U324(tt(),N,X,XS) -> #a__U325(a__isLNat(XS),N,X,XS) #89: #a__U324(tt(),N,X,XS) -> #a__isLNat(XS) #90: #mark(splitAt(X1,X2)) -> #a__splitAt(mark(X1),mark(X2)) #91: #mark(splitAt(X1,X2)) -> #mark(X1) #92: #mark(splitAt(X1,X2)) -> #mark(X2) #93: #a__U282(tt(),N) -> #mark(N) #94: #mark(s(X)) -> #mark(X) #95: #mark(U54(X1,X2,X3)) -> #a__U54(mark(X1),X2,X3) #96: #mark(U54(X1,X2,X3)) -> #mark(X1) #97: #a__isNaturalKind(sel(V1,V2)) -> #a__U231(a__isNaturalKind(V1),V2) #98: #a__isNaturalKind(sel(V1,V2)) -> #a__isNaturalKind(V1) #99: #a__fst(pair(X,Y)) -> #a__U21(a__isLNat(X),X,Y) #100: #a__fst(pair(X,Y)) -> #a__isLNat(X) #101: #mark(U106(X)) -> #a__U106(mark(X)) #102: #mark(U106(X)) -> #mark(X) #103: #a__U293(tt(),N,XS) -> #a__U294(a__isLNatKind(XS),N,XS) #104: #a__U293(tt(),N,XS) -> #a__isLNatKind(XS) #105: #a__U231(tt(),V2) -> #a__U232(a__isLNatKind(V2)) #106: #a__U231(tt(),V2) -> #a__isLNatKind(V2) #107: #mark(U102(X1,X2,X3)) -> #a__U102(mark(X1),X2,X3) #108: #mark(U102(X1,X2,X3)) -> #mark(X1) #109: #mark(isLNatKind(X)) -> #a__isLNatKind(X) #110: #a__isLNat(afterNth(V1,V2)) -> #a__U41(a__isNaturalKind(V1),V1,V2) #111: #a__isLNat(afterNth(V1,V2)) -> #a__isNaturalKind(V1) #112: #mark(U104(X1,X2,X3)) -> #a__U104(mark(X1),X2,X3) #113: #mark(U104(X1,X2,X3)) -> #mark(X1) #114: #mark(U303(X1,X2)) -> #a__U303(mark(X1),X2) #115: #mark(U303(X1,X2)) -> #mark(X1) #116: #mark(U241(X1,X2,X3)) -> #a__U241(mark(X1),X2,X3) #117: #mark(U241(X1,X2,X3)) -> #mark(X1) #118: #mark(U121(X1,X2)) -> #a__U121(mark(X1),X2) #119: #mark(U121(X1,X2)) -> #mark(X1) #120: #a__U291(tt(),N,XS) -> #a__U292(a__isNaturalKind(N),N,XS) #121: #a__U291(tt(),N,XS) -> #a__isNaturalKind(N) #122: #mark(U24(X1,X2)) -> #a__U24(mark(X1),X2) #123: #mark(U24(X1,X2)) -> #mark(X1) #124: #a__U92(tt(),V1) -> #a__U93(a__isLNat(V1)) #125: #a__U92(tt(),V1) -> #a__isLNat(V1) #126: #a__isNatural(head(V1)) -> #a__U181(a__isLNatKind(V1),V1) #127: #a__isNatural(head(V1)) -> #a__isLNatKind(V1) #128: #a__U271(tt(),V2) -> #a__U272(a__isLNatKind(V2)) #129: #a__U271(tt(),V2) -> #a__isLNatKind(V2) #130: #a__U31(tt(),N,XS) -> #a__U32(a__isNaturalKind(N),N,XS) #131: #a__U31(tt(),N,XS) -> #a__isNaturalKind(N) #132: #mark(U271(X1,X2)) -> #a__U271(mark(X1),X2) #133: #mark(U271(X1,X2)) -> #mark(X1) #134: #a__U24(tt(),X) -> #mark(X) #135: #mark(U82(X1,X2)) -> #a__U82(mark(X1),X2) #136: #mark(U82(X1,X2)) -> #mark(X1) #137: #a__U43(tt(),V1,V2) -> #a__U44(a__isLNatKind(V2),V1,V2) #138: #a__U43(tt(),V1,V2) -> #a__isLNatKind(V2) #139: #mark(U43(X1,X2,X3)) -> #a__U43(mark(X1),X2,X3) #140: #mark(U43(X1,X2,X3)) -> #mark(X1) #141: #a__splitAt(0(),XS) -> #a__U311(a__isLNat(XS),XS) #142: #a__splitAt(0(),XS) -> #a__isLNat(XS) #143: #a__U82(tt(),V1) -> #a__U83(a__isPLNat(V1)) #144: #a__U82(tt(),V1) -> #a__isPLNat(V1) #145: #a__U255(tt(),V2) -> #a__U256(a__isLNat(V2)) #146: #a__U255(tt(),V2) -> #a__isLNat(V2) #147: #mark(afterNth(X1,X2)) -> #a__afterNth(mark(X1),mark(X2)) #148: #mark(afterNth(X1,X2)) -> #mark(X1) #149: #mark(afterNth(X1,X2)) -> #mark(X2) #150: #a__U13(tt(),N,XS) -> #a__U14(a__isLNatKind(XS),N,XS) #151: #a__U13(tt(),N,XS) -> #a__isLNatKind(XS) #152: #mark(U251(X1,X2,X3)) -> #a__U251(mark(X1),X2,X3) #153: #mark(U251(X1,X2,X3)) -> #mark(X1) #154: #a__U121(tt(),V2) -> #a__U122(a__isLNatKind(V2)) #155: #a__U121(tt(),V2) -> #a__isLNatKind(V2) #156: #mark(natsFrom(X)) -> #a__natsFrom(mark(X)) #157: #mark(natsFrom(X)) -> #mark(X) #158: #a__U55(tt(),V2) -> #a__U56(a__isLNat(V2)) #159: #a__U55(tt(),V2) -> #a__isLNat(V2) #160: #mark(U55(X1,X2)) -> #a__U55(mark(X1),X2) #161: #mark(U55(X1,X2)) -> #mark(X1) #162: #mark(U105(X1,X2)) -> #a__U105(mark(X1),X2) #163: #mark(U105(X1,X2)) -> #mark(X1) #164: #a__U281(tt(),N) -> #a__U282(a__isNaturalKind(N),N) #165: #a__U281(tt(),N) -> #a__isNaturalKind(N) #166: #mark(U344(X1,X2,X3)) -> #a__U344(mark(X1),X2,X3) #167: #mark(U344(X1,X2,X3)) -> #mark(X1) #168: #mark(U242(X1,X2,X3)) -> #a__U242(mark(X1),X2,X3) #169: #mark(U242(X1,X2,X3)) -> #mark(X1) #170: #a__U326(tt(),N,X,XS) -> #a__U327(a__splitAt(mark(N),mark(XS)),X) #171: #a__U326(tt(),N,X,XS) -> #a__splitAt(mark(N),mark(XS)) #172: #a__U326(tt(),N,X,XS) -> #mark(N) #173: #a__U326(tt(),N,X,XS) -> #mark(XS) #174: #mark(U14(X1,X2,X3)) -> #a__U14(mark(X1),X2,X3) #175: #mark(U14(X1,X2,X3)) -> #mark(X1) #176: #mark(U211(X)) -> #a__U211(mark(X)) #177: #mark(U211(X)) -> #mark(X) #178: #a__U91(tt(),V1) -> #a__U92(a__isLNatKind(V1),V1) #179: #a__U91(tt(),V1) -> #a__isLNatKind(V1) #180: #a__U51(tt(),V1,V2) -> #a__U52(a__isNaturalKind(V1),V1,V2) #181: #a__U51(tt(),V1,V2) -> #a__isNaturalKind(V1) #182: #a__U191(tt(),V1) -> #a__U192(a__isNaturalKind(V1),V1) #183: #a__U191(tt(),V1) -> #a__isNaturalKind(V1) #184: #a__isNatural(sel(V1,V2)) -> #a__U201(a__isNaturalKind(V1),V1,V2) #185: #a__isNatural(sel(V1,V2)) -> #a__isNaturalKind(V1) #186: #a__U32(tt(),N,XS) -> #a__U33(a__isLNat(XS),N,XS) #187: #a__U32(tt(),N,XS) -> #a__isLNat(XS) #188: #mark(tail(X)) -> #a__tail(mark(X)) #189: #mark(tail(X)) -> #mark(X) #190: #mark(U327(X1,X2)) -> #a__U327(mark(X1),X2) #191: #mark(U327(X1,X2)) -> #mark(X1) #192: #a__isLNatKind(snd(V1)) -> #a__U151(a__isPLNatKind(V1)) #193: #a__isLNatKind(snd(V1)) -> #a__isPLNatKind(V1) #194: #a__U333(tt(),XS) -> #a__U334(a__isLNatKind(XS),XS) #195: #a__U333(tt(),XS) -> #a__isLNatKind(XS) #196: #a__isLNat(fst(V1)) -> #a__U61(a__isPLNatKind(V1),V1) #197: #a__isLNat(fst(V1)) -> #a__isPLNatKind(V1) #198: #a__U33(tt(),N,XS) -> #a__U34(a__isLNatKind(XS),N) #199: #a__U33(tt(),N,XS) -> #a__isLNatKind(XS) #200: #a__U245(tt(),V2) -> #a__U246(a__isLNat(V2)) #201: #a__U245(tt(),V2) -> #a__isLNat(V2) #202: #a__U53(tt(),V1,V2) -> #a__U54(a__isLNatKind(V2),V1,V2) #203: #a__U53(tt(),V1,V2) -> #a__isLNatKind(V2) #204: #mark(U252(X1,X2,X3)) -> #a__U252(mark(X1),X2,X3) #205: #mark(U252(X1,X2,X3)) -> #mark(X1) #206: #mark(U246(X)) -> #a__U246(mark(X)) #207: #mark(U246(X)) -> #mark(X) #208: #a__U312(tt(),XS) -> #mark(XS) #209: #mark(U262(X)) -> #a__U262(mark(X)) #210: #mark(U262(X)) -> #mark(X) #211: #a__U62(tt(),V1) -> #a__U63(a__isPLNat(V1)) #212: #a__U62(tt(),V1) -> #a__isPLNat(V1) #213: #a__U205(tt(),V2) -> #a__U206(a__isLNat(V2)) #214: #a__U205(tt(),V2) -> #a__isLNat(V2) #215: #mark(U13(X1,X2,X3)) -> #a__U13(mark(X1),X2,X3) #216: #mark(U13(X1,X2,X3)) -> #mark(X1) #217: #mark(U91(X1,X2)) -> #a__U91(mark(X1),X2) #218: #mark(U91(X1,X2)) -> #mark(X1) #219: #mark(U293(X1,X2,X3)) -> #a__U293(mark(X1),X2,X3) #220: #mark(U293(X1,X2,X3)) -> #mark(X1) #221: #a__U331(tt(),N,XS) -> #a__U332(a__isNaturalKind(N),XS) #222: #a__U331(tt(),N,XS) -> #a__isNaturalKind(N) #223: #a__U42(tt(),V1,V2) -> #a__U43(a__isLNatKind(V2),V1,V2) #224: #a__U42(tt(),V1,V2) -> #a__isLNatKind(V2) #225: #a__isNatural(s(V1)) -> #a__U191(a__isNaturalKind(V1),V1) #226: #a__isNatural(s(V1)) -> #a__isNaturalKind(V1) #227: #a__U334(tt(),XS) -> #mark(XS) #228: #mark(cons(X1,X2)) -> #mark(X1) #229: #mark(U73(X)) -> #a__U73(mark(X)) #230: #mark(U73(X)) -> #mark(X) #231: #mark(U255(X1,X2)) -> #a__U255(mark(X1),X2) #232: #mark(U255(X1,X2)) -> #mark(X1) #233: #a__U81(tt(),V1) -> #a__U82(a__isPLNatKind(V1),V1) #234: #a__U81(tt(),V1) -> #a__isPLNatKind(V1) #235: #mark(U204(X1,X2,X3)) -> #a__U204(mark(X1),X2,X3) #236: #mark(U204(X1,X2,X3)) -> #mark(X1) #237: #a__U294(tt(),N,XS) -> #a__head(a__afterNth(mark(N),mark(XS))) #238: #a__U294(tt(),N,XS) -> #a__afterNth(mark(N),mark(XS)) #239: #a__U294(tt(),N,XS) -> #mark(N) #240: #a__U294(tt(),N,XS) -> #mark(XS) #241: #a__U204(tt(),V1,V2) -> #a__U205(a__isNatural(V1),V2) #242: #a__U204(tt(),V1,V2) -> #a__isNatural(V1) #243: #mark(U44(X1,X2,X3)) -> #a__U44(mark(X1),X2,X3) #244: #mark(U44(X1,X2,X3)) -> #mark(X1) #245: #mark(U245(X1,X2)) -> #a__U245(mark(X1),X2) #246: #mark(U245(X1,X2)) -> #mark(X1) #247: #a__U253(tt(),V1,V2) -> #a__U254(a__isLNatKind(V2),V1,V2) #248: #a__U253(tt(),V1,V2) -> #a__isLNatKind(V2) #249: #a__U192(tt(),V1) -> #a__U193(a__isNatural(V1)) #250: #a__U192(tt(),V1) -> #a__isNatural(V1) #251: #a__isLNatKind(take(V1,V2)) -> #a__U171(a__isNaturalKind(V1),V2) #252: #a__isLNatKind(take(V1,V2)) -> #a__isNaturalKind(V1) #253: #mark(U122(X)) -> #a__U122(mark(X)) #254: #mark(U122(X)) -> #mark(X) #255: #a__isLNatKind(tail(V1)) -> #a__U161(a__isLNatKind(V1)) #256: #a__isLNatKind(tail(V1)) -> #a__isLNatKind(V1) #257: #mark(U191(X1,X2)) -> #a__U191(mark(X1),X2) #258: #mark(U191(X1,X2)) -> #mark(X1) #259: #a__isLNatKind(fst(V1)) -> #a__U131(a__isPLNatKind(V1)) #260: #a__isLNatKind(fst(V1)) -> #a__isPLNatKind(V1) #261: #mark(U171(X1,X2)) -> #a__U171(mark(X1),X2) #262: #mark(U171(X1,X2)) -> #mark(X1) #263: #a__U41(tt(),V1,V2) -> #a__U42(a__isNaturalKind(V1),V1,V2) #264: #a__U41(tt(),V1,V2) -> #a__isNaturalKind(V1) #265: #a__U11(tt(),N,XS) -> #a__U12(a__isNaturalKind(N),N,XS) #266: #a__U11(tt(),N,XS) -> #a__isNaturalKind(N) #267: #mark(U256(X)) -> #a__U256(mark(X)) #268: #mark(U256(X)) -> #mark(X) #269: #mark(U103(X1,X2,X3)) -> #a__U103(mark(X1),X2,X3) #270: #mark(U103(X1,X2,X3)) -> #mark(X1) #271: #mark(U52(X1,X2,X3)) -> #a__U52(mark(X1),X2,X3) #272: #mark(U52(X1,X2,X3)) -> #mark(X1) #273: #a__isNaturalKind(head(V1)) -> #a__U211(a__isLNatKind(V1)) #274: #a__isNaturalKind(head(V1)) -> #a__isLNatKind(V1) #275: #mark(U304(X1,X2)) -> #a__U304(mark(X1),X2) #276: #mark(U304(X1,X2)) -> #mark(X1) #277: #a__U12(tt(),N,XS) -> #a__U13(a__isLNat(XS),N,XS) #278: #a__U12(tt(),N,XS) -> #a__isLNat(XS) #279: #a__U45(tt(),V2) -> #a__U46(a__isLNat(V2)) #280: #a__U45(tt(),V2) -> #a__isLNat(V2) #281: #mark(U324(X1,X2,X3,X4)) -> #a__U324(mark(X1),X2,X3,X4) #282: #mark(U324(X1,X2,X3,X4)) -> #mark(X1) #283: #mark(U172(X)) -> #a__U172(mark(X)) #284: #mark(U172(X)) -> #mark(X) #285: #a__isLNat(natsFrom(V1)) -> #a__U71(a__isNaturalKind(V1),V1) #286: #a__isLNat(natsFrom(V1)) -> #a__isNaturalKind(V1) #287: #a__U302(tt(),Y) -> #a__U303(a__isLNat(Y),Y) #288: #a__U302(tt(),Y) -> #a__isLNat(Y) #289: #a__U21(tt(),X,Y) -> #a__U22(a__isLNatKind(X),X,Y) #290: #a__U21(tt(),X,Y) -> #a__isLNatKind(X) #291: #mark(isPLNatKind(X)) -> #a__isPLNatKind(X) #292: #a__U322(tt(),N,X,XS) -> #a__U323(a__isNatural(X),N,X,XS) #293: #a__U322(tt(),N,X,XS) -> #a__isNatural(X) #294: #mark(U111(X1,X2)) -> #a__U111(mark(X1),X2) #295: #mark(U111(X1,X2)) -> #mark(X1) #296: #mark(U203(X1,X2,X3)) -> #a__U203(mark(X1),X2,X3) #297: #mark(U203(X1,X2,X3)) -> #mark(X1) #298: #a__isLNat(snd(V1)) -> #a__U81(a__isPLNatKind(V1),V1) #299: #a__isLNat(snd(V1)) -> #a__isPLNatKind(V1) #300: #a__U105(tt(),V2) -> #a__U106(a__isLNat(V2)) #301: #a__U105(tt(),V2) -> #a__isLNat(V2) #302: #a__U244(tt(),V1,V2) -> #a__U245(a__isLNat(V1),V2) #303: #a__U244(tt(),V1,V2) -> #a__isLNat(V1) #304: #a__U303(tt(),Y) -> #a__U304(a__isLNatKind(Y),Y) #305: #a__U303(tt(),Y) -> #a__isLNatKind(Y) #306: #a__tail(cons(N,XS)) -> #a__U331(a__isNatural(N),N,XS) #307: #a__tail(cons(N,XS)) -> #a__isNatural(N) #308: #a__U202(tt(),V1,V2) -> #a__U203(a__isLNatKind(V2),V1,V2) #309: #a__U202(tt(),V1,V2) -> #a__isLNatKind(V2) #310: #mark(U302(X1,X2)) -> #a__U302(mark(X1),X2) #311: #mark(U302(X1,X2)) -> #mark(X1) #312: #mark(U291(X1,X2,X3)) -> #a__U291(mark(X1),X2,X3) #313: #mark(U291(X1,X2,X3)) -> #mark(X1) #314: #a__U182(tt(),V1) -> #a__U183(a__isLNat(V1)) #315: #a__U182(tt(),V1) -> #a__isLNat(V1) #316: #a__isLNatKind(natsFrom(V1)) -> #a__U141(a__isNaturalKind(V1)) #317: #a__isLNatKind(natsFrom(V1)) -> #a__isNaturalKind(V1) #318: #mark(snd(X)) -> #a__snd(mark(X)) #319: #mark(snd(X)) -> #mark(X) #320: #mark(U45(X1,X2)) -> #a__U45(mark(X1),X2) #321: #mark(U45(X1,X2)) -> #mark(X1) #322: #mark(U334(X1,X2)) -> #a__U334(mark(X1),X2) #323: #mark(U334(X1,X2)) -> #mark(X1) #324: #mark(take(X1,X2)) -> #a__take(mark(X1),mark(X2)) #325: #mark(take(X1,X2)) -> #mark(X1) #326: #mark(take(X1,X2)) -> #mark(X2) #327: #mark(U141(X)) -> #a__U141(mark(X)) #328: #mark(U141(X)) -> #mark(X) #329: #mark(U202(X1,X2,X3)) -> #a__U202(mark(X1),X2,X3) #330: #mark(U202(X1,X2,X3)) -> #mark(X1) #331: #a__U341(tt(),N,XS) -> #a__U342(a__isNaturalKind(N),N,XS) #332: #a__U341(tt(),N,XS) -> #a__isNaturalKind(N) #333: #a__U344(tt(),N,XS) -> #a__fst(a__splitAt(mark(N),mark(XS))) #334: #a__U344(tt(),N,XS) -> #a__splitAt(mark(N),mark(XS)) #335: #a__U344(tt(),N,XS) -> #mark(N) #336: #a__U344(tt(),N,XS) -> #mark(XS) #337: #mark(U281(X1,X2)) -> #a__U281(mark(X1),X2) #338: #mark(U281(X1,X2)) -> #mark(X1) #339: #mark(U231(X1,X2)) -> #a__U231(mark(X1),X2) #340: #mark(U231(X1,X2)) -> #mark(X1) #341: #mark(isNatural(X)) -> #a__isNatural(X) #342: #mark(U342(X1,X2,X3)) -> #a__U342(mark(X1),X2,X3) #343: #mark(U342(X1,X2,X3)) -> #mark(X1) #344: #a__U201(tt(),V1,V2) -> #a__U202(a__isNaturalKind(V1),V1,V2) #345: #a__U201(tt(),V1,V2) -> #a__isNaturalKind(V1) #346: #mark(U63(X)) -> #a__U63(mark(X)) #347: #mark(U63(X)) -> #mark(X) #348: #a__isNaturalKind(s(V1)) -> #a__U221(a__isNaturalKind(V1)) #349: #a__isNaturalKind(s(V1)) -> #a__isNaturalKind(V1) #350: #a__sel(N,XS) -> #a__U291(a__isNatural(N),N,XS) #351: #a__sel(N,XS) -> #a__isNatural(N) #352: #a__isPLNatKind(splitAt(V1,V2)) -> #a__U271(a__isNaturalKind(V1),V2) #353: #a__isPLNatKind(splitAt(V1,V2)) -> #a__isNaturalKind(V1) #354: #mark(U12(X1,X2,X3)) -> #a__U12(mark(X1),X2,X3) #355: #mark(U12(X1,X2,X3)) -> #mark(X1) #356: #mark(U343(X1,X2,X3)) -> #a__U343(mark(X1),X2,X3) #357: #mark(U343(X1,X2,X3)) -> #mark(X1) #358: #mark(U206(X)) -> #a__U206(mark(X)) #359: #mark(U206(X)) -> #mark(X) #360: #mark(U101(X1,X2,X3)) -> #a__U101(mark(X1),X2,X3) #361: #mark(U101(X1,X2,X3)) -> #mark(X1) #362: #a__U292(tt(),N,XS) -> #a__U293(a__isLNat(XS),N,XS) #363: #a__U292(tt(),N,XS) -> #a__isLNat(XS) #364: #mark(U261(X1,X2)) -> #a__U261(mark(X1),X2) #365: #mark(U261(X1,X2)) -> #mark(X1) #366: #a__isLNat(cons(V1,V2)) -> #a__U51(a__isNaturalKind(V1),V1,V2) #367: #a__isLNat(cons(V1,V2)) -> #a__isNaturalKind(V1) #368: #mark(U83(X)) -> #a__U83(mark(X)) #369: #mark(U83(X)) -> #mark(X) #370: #mark(U71(X1,X2)) -> #a__U71(mark(X1),X2) #371: #mark(U71(X1,X2)) -> #mark(X1) #372: #mark(U244(X1,X2,X3)) -> #a__U244(mark(X1),X2,X3) #373: #mark(U244(X1,X2,X3)) -> #mark(X1) #374: #mark(U32(X1,X2,X3)) -> #a__U32(mark(X1),X2,X3) #375: #mark(U32(X1,X2,X3)) -> #mark(X1) #376: #mark(U312(X1,X2)) -> #a__U312(mark(X1),X2) #377: #mark(U312(X1,X2)) -> #mark(X1) #378: #mark(U151(X)) -> #a__U151(mark(X)) #379: #mark(U151(X)) -> #mark(X) #380: #mark(U311(X1,X2)) -> #a__U311(mark(X1),X2) #381: #mark(U311(X1,X2)) -> #mark(X1) #382: #a__U171(tt(),V2) -> #a__U172(a__isLNatKind(V2)) #383: #a__U171(tt(),V2) -> #a__isLNatKind(V2) #384: #a__natsFrom(N) -> #a__U281(a__isNatural(N),N) #385: #a__natsFrom(N) -> #a__isNatural(N) #386: #a__isLNatKind(cons(V1,V2)) -> #a__U121(a__isNaturalKind(V1),V2) #387: #a__isLNatKind(cons(V1,V2)) -> #a__isNaturalKind(V1) #388: #mark(U92(X1,X2)) -> #a__U92(mark(X1),X2) #389: #mark(U92(X1,X2)) -> #mark(X1) #390: #mark(U61(X1,X2)) -> #a__U61(mark(X1),X2) #391: #mark(U61(X1,X2)) -> #mark(X1) #392: #mark(U272(X)) -> #a__U272(mark(X)) #393: #mark(U272(X)) -> #mark(X) #394: #mark(U221(X)) -> #a__U221(mark(X)) #395: #mark(U221(X)) -> #mark(X) #396: #mark(U205(X1,X2)) -> #a__U205(mark(X1),X2) #397: #mark(U205(X1,X2)) -> #mark(X1) #398: #mark(U181(X1,X2)) -> #a__U181(mark(X1),X2) #399: #mark(U181(X1,X2)) -> #mark(X1) #400: #mark(pair(X1,X2)) -> #mark(X1) #401: #mark(pair(X1,X2)) -> #mark(X2) #402: #a__U301(tt(),X,Y) -> #a__U302(a__isLNatKind(X),Y) #403: #a__U301(tt(),X,Y) -> #a__isLNatKind(X) #404: #mark(U41(X1,X2,X3)) -> #a__U41(mark(X1),X2,X3) #405: #mark(U41(X1,X2,X3)) -> #mark(X1) #406: #mark(U31(X1,X2,X3)) -> #a__U31(mark(X1),X2,X3) #407: #mark(U31(X1,X2,X3)) -> #mark(X1) #408: #a__U61(tt(),V1) -> #a__U62(a__isPLNatKind(V1),V1) #409: #a__U61(tt(),V1) -> #a__isPLNatKind(V1) #410: #a__U342(tt(),N,XS) -> #a__U343(a__isLNat(XS),N,XS) #411: #a__U342(tt(),N,XS) -> #a__isLNat(XS) #412: #mark(U34(X1,X2)) -> #a__U34(mark(X1),X2) #413: #mark(U34(X1,X2)) -> #mark(X1) #414: #mark(U193(X)) -> #a__U193(mark(X)) #415: #mark(U193(X)) -> #mark(X) #416: #a__isLNat(take(V1,V2)) -> #a__U101(a__isNaturalKind(V1),V1,V2) #417: #a__isLNat(take(V1,V2)) -> #a__isNaturalKind(V1) #418: #mark(U282(X1,X2)) -> #a__U282(mark(X1),X2) #419: #mark(U282(X1,X2)) -> #mark(X1) #420: #a__U311(tt(),XS) -> #a__U312(a__isLNatKind(XS),XS) #421: #a__U311(tt(),XS) -> #a__isLNatKind(XS) #422: #mark(U322(X1,X2,X3,X4)) -> #a__U322(mark(X1),X2,X3,X4) #423: #mark(U322(X1,X2,X3,X4)) -> #mark(X1) #424: #a__U181(tt(),V1) -> #a__U182(a__isLNatKind(V1),V1) #425: #a__U181(tt(),V1) -> #a__isLNatKind(V1) #426: #a__U103(tt(),V1,V2) -> #a__U104(a__isLNatKind(V2),V1,V2) #427: #a__U103(tt(),V1,V2) -> #a__isLNatKind(V2) #428: #mark(isLNat(X)) -> #a__isLNat(X) #429: #mark(U341(X1,X2,X3)) -> #a__U341(mark(X1),X2,X3) #430: #mark(U341(X1,X2,X3)) -> #mark(X1) #431: #a__U327(pair(YS,ZS),X) -> #mark(X) #432: #a__U327(pair(YS,ZS),X) -> #mark(ZS) #433: #a__U101(tt(),V1,V2) -> #a__U102(a__isNaturalKind(V1),V1,V2) #434: #a__U101(tt(),V1,V2) -> #a__isNaturalKind(V1) #435: #a__isPLNat(splitAt(V1,V2)) -> #a__U251(a__isNaturalKind(V1),V1,V2) #436: #a__isPLNat(splitAt(V1,V2)) -> #a__isNaturalKind(V1) #437: #a__isLNatKind(afterNth(V1,V2)) -> #a__U111(a__isNaturalKind(V1),V2) #438: #a__isLNatKind(afterNth(V1,V2)) -> #a__isNaturalKind(V1) #439: #mark(U232(X)) -> #a__U232(mark(X)) #440: #mark(U232(X)) -> #mark(X) #441: #mark(fst(X)) -> #a__fst(mark(X)) #442: #mark(fst(X)) -> #mark(X) #443: #mark(U326(X1,X2,X3,X4)) -> #a__U326(mark(X1),X2,X3,X4) #444: #mark(U326(X1,X2,X3,X4)) -> #mark(X1) #445: #mark(U253(X1,X2,X3)) -> #a__U253(mark(X1),X2,X3) #446: #mark(U253(X1,X2,X3)) -> #mark(X1) #447: #mark(U11(X1,X2,X3)) -> #a__U11(mark(X1),X2,X3) #448: #mark(U11(X1,X2,X3)) -> #mark(X1) #449: #a__U111(tt(),V2) -> #a__U112(a__isLNatKind(V2)) #450: #a__U111(tt(),V2) -> #a__isLNatKind(V2) #451: #mark(U254(X1,X2,X3)) -> #a__U254(mark(X1),X2,X3) #452: #mark(U254(X1,X2,X3)) -> #mark(X1) #453: #mark(isNaturalKind(X)) -> #a__isNaturalKind(X) #454: #mark(U131(X)) -> #a__U131(mark(X)) #455: #mark(U131(X)) -> #mark(X) #456: #mark(U292(X1,X2,X3)) -> #a__U292(mark(X1),X2,X3) #457: #mark(U292(X1,X2,X3)) -> #mark(X1) #458: #a__isPLNatKind(pair(V1,V2)) -> #a__U261(a__isLNatKind(V1),V2) #459: #a__isPLNatKind(pair(V1,V2)) -> #a__isLNatKind(V1) #460: #a__isLNat(tail(V1)) -> #a__U91(a__isLNatKind(V1),V1) #461: #a__isLNat(tail(V1)) -> #a__isLNatKind(V1) #462: #mark(sel(X1,X2)) -> #a__sel(mark(X1),mark(X2)) #463: #mark(sel(X1,X2)) -> #mark(X1) #464: #mark(sel(X1,X2)) -> #mark(X2) #465: #mark(U192(X1,X2)) -> #a__U192(mark(X1),X2) #466: #mark(U192(X1,X2)) -> #mark(X1) #467: #mark(U301(X1,X2,X3)) -> #a__U301(mark(X1),X2,X3) #468: #mark(U301(X1,X2,X3)) -> #mark(X1) #469: #a__U14(tt(),N,XS) -> #a__snd(a__splitAt(mark(N),mark(XS))) #470: #a__U14(tt(),N,XS) -> #a__splitAt(mark(N),mark(XS)) #471: #a__U14(tt(),N,XS) -> #mark(N) #472: #a__U14(tt(),N,XS) -> #mark(XS) #473: #a__snd(pair(X,Y)) -> #a__U301(a__isLNat(X),X,Y) #474: #a__snd(pair(X,Y)) -> #a__isLNat(X) #475: #mark(U93(X)) -> #a__U93(mark(X)) #476: #mark(U93(X)) -> #mark(X) #477: #mark(U22(X1,X2,X3)) -> #a__U22(mark(X1),X2,X3) #478: #mark(U22(X1,X2,X3)) -> #mark(X1) #479: #a__U71(tt(),V1) -> #a__U72(a__isNaturalKind(V1),V1) #480: #a__U71(tt(),V1) -> #a__isNaturalKind(V1) #481: #mark(U56(X)) -> #a__U56(mark(X)) #482: #mark(U56(X)) -> #mark(X) #483: #mark(head(X)) -> #a__head(mark(X)) #484: #mark(head(X)) -> #mark(X) #485: #a__U104(tt(),V1,V2) -> #a__U105(a__isNatural(V1),V2) #486: #a__U104(tt(),V1,V2) -> #a__isNatural(V1) #487: #mark(U21(X1,X2,X3)) -> #a__U21(mark(X1),X2,X3) #488: #mark(U21(X1,X2,X3)) -> #mark(X1) #489: #a__U72(tt(),V1) -> #a__U73(a__isNatural(V1)) #490: #a__U72(tt(),V1) -> #a__isNatural(V1) #491: #a__U332(tt(),XS) -> #a__U333(a__isLNat(XS),XS) #492: #a__U332(tt(),XS) -> #a__isLNat(XS) #493: #a__U254(tt(),V1,V2) -> #a__U255(a__isNatural(V1),V2) #494: #a__U254(tt(),V1,V2) -> #a__isNatural(V1) #495: #mark(U201(X1,X2,X3)) -> #a__U201(mark(X1),X2,X3) #496: #mark(U201(X1,X2,X3)) -> #mark(X1) #497: #mark(U332(X1,X2)) -> #a__U332(mark(X1),X2) #498: #mark(U332(X1,X2)) -> #mark(X1) Number of SCCs: 3, DPs: 322, edges: 25736 SCC { #63 #97 #98 #106 #129 #155 #193 #251 #252 #256 #260 #274 #317 #349 #352 #353 #383 #386 #387 #437 #438 #450 #458 #459 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U291(x1,x2,x3) weight: 0 #a__U193(x1) weight: 0 a__U83(x1) weight: 0 U231(x1,x2) weight: (/ 3 8) + x1 U301(x1,x2,x3) weight: 0 a__U293(x1,x2,x3) weight: 0 a__U241(x1,x2,x3) weight: 0 U204(x1,x2,x3) weight: 0 a__U324(x1,x2,x3,x4) weight: 0 a__U302(x1,x2) weight: 0 #a__isNaturalKind(x1) weight: x1 a__U325(x1,x2,x3,x4) weight: 0 a__U151(x1) weight: (/ 1 4) a__U292(x1,x2,x3) weight: 0 #a__U73(x1) weight: 0 #a__U131(x1) weight: 0 a__U63(x1) weight: 0 U21(x1,x2,x3) weight: 0 U261(x1,x2) weight: (/ 3 8) + x1 + x2 a__U102(x1,x2,x3) weight: 0 U254(x1,x2,x3) weight: 0 U333(x1,x2) weight: 0 #a__U82(x1,x2) weight: 0 a__U332(x1,x2) weight: 0 a__U45(x1,x2) weight: 0 U193(x1) weight: 0 #a__U72(x1,x2) weight: 0 #a__U242(x1,x2,x3) weight: 0 a__U246(x1) weight: 0 U161(x1) weight: (/ 3 8) + x1 #a__U321(x1,x2,x3,x4) weight: 0 #a__U71(x1,x2) weight: 0 a__U232(x1) weight: (/ 3 8) U182(x1,x2) weight: 0 #a__U291(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 a__U171(x1,x2) weight: (/ 1 4) + x2 #a__U92(x1,x2) weight: 0 a__U104(x1,x2,x3) weight: 0 a__U294(x1,x2,x3) weight: 0 a__U182(x1,x2) weight: 0 a__U191(x1,x2) weight: 0 a__U281(x1,x2) weight: 0 U243(x1,x2,x3) weight: 0 a__U245(x1,x2) weight: 0 #a__U112(x1) weight: 0 s(x1) weight: (/ 1 8) + x1 U105(x1,x2) weight: 0 U303(x1,x2) weight: 0 #a__U292(x1,x2,x3) weight: 0 a__U24(x1,x2) weight: 0 #a__U341(x1,x2,x3) weight: 0 #a__U31(x1,x2,x3) weight: 0 a__U243(x1,x2,x3) weight: 0 #a__U33(x1,x2,x3) weight: 0 #a__U93(x1) weight: 0 #a__head(x1) weight: 0 U192(x1,x2) weight: 0 #a__U253(x1,x2,x3) weight: 0 U24(x1,x2) weight: 0 a__U33(x1,x2,x3) weight: 0 U106(x1) weight: 0 #a__U24(x1,x2) weight: 0 #a__natsFrom(x1) weight: 0 isPLNatKind(x1) weight: (/ 1 4) + x1 #a__U252(x1,x2,x3) weight: 0 #a__U256(x1) weight: 0 a__U244(x1,x2,x3) weight: 0 a__U343(x1,x2,x3) weight: 0 U242(x1,x2,x3) weight: 0 #a__U303(x1,x2) weight: 0 U262(x1) weight: (/ 1 2) + x1 U244(x1,x2,x3) weight: 0 U272(x1) weight: (/ 1 2) + x1 U56(x1) weight: 0 #a__U191(x1,x2) weight: 0 #a__U272(x1) weight: 0 #a__U23(x1,x2,x3) weight: 0 a__U55(x1,x2) weight: 0 isPLNat(x1) weight: 0 #a__snd(x1) weight: 0 a__U331(x1,x2,x3) weight: 0 #a__U312(x1,x2) weight: 0 a__afterNth(x1,x2) weight: 0 U42(x1,x2,x3) weight: 0 U91(x1,x2) weight: 0 U221(x1) weight: (/ 3 8) + x1 U293(x1,x2,x3) weight: 0 a__U73(x1) weight: 0 #a__U106(x1) weight: 0 U325(x1,x2,x3,x4) weight: 0 a__U82(x1,x2) weight: 0 #a__U182(x1,x2) weight: 0 take(x1,x2) weight: (/ 1 4) + x1 + x2 #a__U14(x1,x2,x3) weight: 0 U71(x1,x2) weight: 0 a__U62(x1,x2) weight: 0 a__U44(x1,x2,x3) weight: 0 U131(x1) weight: (/ 3 8) + x1 U206(x1) weight: 0 a__U221(x1) weight: (/ 1 4) U101(x1,x2,x3) weight: 0 #a__U43(x1,x2,x3) weight: 0 #a__U334(x1,x2) weight: 0 pair(x1,x2) weight: (/ 1 8) + x1 + x2 U255(x1,x2) weight: 0 #a__U326(x1,x2,x3,x4) weight: 0 a__U261(x1,x2) weight: (/ 1 4) fst(x1) weight: (/ 1 4) + x1 U111(x1,x2) weight: (/ 3 8) + x1 + x2 U43(x1,x2,x3) weight: 0 #a__U13(x1,x2,x3) weight: 0 a__U121(x1,x2) weight: (/ 1 4) + x2 a__U262(x1) weight: (/ 3 8) #a__U246(x1) weight: 0 #a__U44(x1,x2,x3) weight: 0 #a__U204(x1,x2,x3) weight: 0 U103(x1,x2,x3) weight: 0 a__U111(x1,x2) weight: (/ 1 4) a__U272(x1) weight: (/ 3 8) natsFrom(x1) weight: (/ 1 8) + x1 U281(x1,x2) weight: 0 #a__U103(x1,x2,x3) weight: 0 #a__U301(x1,x2,x3) weight: 0 U44(x1,x2,x3) weight: 0 U55(x1,x2) weight: 0 #a__U46(x1) weight: 0 a__snd(x1) weight: 0 a__U252(x1,x2,x3) weight: 0 U253(x1,x2,x3) weight: 0 U312(x1,x2) weight: 0 #a__U206(x1) weight: 0 #a__U181(x1,x2) weight: 0 a__U193(x1) weight: 0 a__U271(x1,x2) weight: (/ 1 4) #a__U51(x1,x2,x3) weight: 0 U341(x1,x2,x3) weight: 0 a__U254(x1,x2,x3) weight: 0 U23(x1,x2,x3) weight: 0 U292(x1,x2,x3) weight: 0 U342(x1,x2,x3) weight: 0 a__U172(x1) weight: (/ 3 8) U63(x1) weight: 0 #a__U56(x1) weight: 0 #a__U344(x1,x2,x3) weight: 0 a__U22(x1,x2,x3) weight: 0 U172(x1) weight: (/ 1 2) + x1 U93(x1) weight: 0 splitAt(x1,x2) weight: (/ 1 8) + x1 + x2 isNaturalKind(x1) weight: (/ 1 4) + x1 U326(x1,x2,x3,x4) weight: 0 #a__U323(x1,x2,x3,x4) weight: 0 a__U106(x1) weight: 0 U72(x1,x2) weight: 0 #a__U11(x1,x2,x3) weight: 0 a__U291(x1,x2,x3) weight: 0 U241(x1,x2,x3) weight: 0 U34(x1,x2) weight: 0 a__U192(x1,x2) weight: 0 a__U31(x1,x2,x3) weight: 0 a__U51(x1,x2,x3) weight: 0 a__U253(x1,x2,x3) weight: 0 a__U81(x1,x2) weight: 0 #a__U53(x1,x2,x3) weight: 0 #a__U205(x1,x2) weight: 0 #a__take(x1,x2) weight: 0 #a__U172(x1) weight: 0 #a__U255(x1,x2) weight: 0 U12(x1,x2,x3) weight: 0 a__U43(x1,x2,x3) weight: 0 U271(x1,x2) weight: (/ 3 8) + x1 + x2 a__U231(x1,x2) weight: (/ 1 4) + x2 #a__U232(x1) weight: 0 #a__isLNatKind(x1) weight: (/ 1 8) + x1 #a__U62(x1,x2) weight: 0 a__U321(x1,x2,x3,x4) weight: 0 a__U206(x1) weight: 0 isNatural(x1) weight: 0 U302(x1,x2) weight: 0 U54(x1,x2,x3) weight: 0 #a__U42(x1,x2,x3) weight: 0 #a__U183(x1) weight: 0 a__U41(x1,x2,x3) weight: 0 U232(x1) weight: (/ 1 2) + x1 #a__U262(x1) weight: 0 #a__U122(x1) weight: 0 #a__U12(x1,x2,x3) weight: 0 U205(x1,x2) weight: 0 a__U205(x1,x2) weight: 0 U201(x1,x2,x3) weight: 0 U104(x1,x2,x3) weight: 0 a__U122(x1) weight: (/ 3 8) a__U14(x1,x2,x3) weight: 0 #a__U81(x1,x2) weight: 0 #a__U21(x1,x2,x3) weight: 0 a__U161(x1) weight: (/ 1 4) #a__U61(x1,x2) weight: 0 #a__U333(x1,x2) weight: 0 a__U34(x1,x2) weight: 0 U252(x1,x2,x3) weight: 0 #a__U261(x1,x2) weight: (/ 1 4) + x2 U141(x1) weight: (/ 3 8) + x1 a__fst(x1) weight: 0 tail(x1) weight: (/ 1 8) + x1 a__natsFrom(x1) weight: 0 #a__U302(x1,x2) weight: 0 U83(x1) weight: 0 #a__U294(x1,x2,x3) weight: 0 #mark(x1) weight: 0 a__U204(x1,x2,x3) weight: 0 0() weight: 0 #a__U211(x1) weight: 0 U294(x1,x2,x3) weight: 0 #a__U244(x1,x2,x3) weight: 0 a__isLNat(x1) weight: 0 U191(x1,x2) weight: 0 U343(x1,x2,x3) weight: 0 a__U251(x1,x2,x3) weight: 0 U73(x1) weight: 0 #a__U282(x1,x2) weight: 0 a__U21(x1,x2,x3) weight: 0 U332(x1,x2) weight: 0 a__U311(x1,x2) weight: 0 U171(x1,x2) weight: (/ 3 8) + x1 a__U32(x1,x2,x3) weight: 0 a__U91(x1,x2) weight: 0 #a__U231(x1,x2) weight: (/ 1 4) + x2 sel(x1,x2) weight: (/ 3 8) + x1 + x2 U202(x1,x2,x3) weight: 0 afterNth(x1,x2) weight: (/ 1 4) + x1 + x2 #a__U151(x1) weight: 0 #a__U111(x1,x2) weight: (/ 1 4) + x2 #a__U161(x1) weight: 0 a__U242(x1,x2,x3) weight: 0 #a__U141(x1) weight: 0 nil() weight: 0 a__splitAt(x1,x2) weight: 0 isLNat(x1) weight: 0 U246(x1) weight: 0 #a__U245(x1,x2) weight: 0 U62(x1,x2) weight: 0 #a__U52(x1,x2,x3) weight: 0 a__U211(x1) weight: (/ 1 4) #a__U102(x1,x2,x3) weight: 0 U304(x1,x2) weight: 0 U45(x1,x2) weight: 0 #a__sel(x1,x2) weight: 0 mark(x1) weight: 0 U151(x1) weight: (/ 3 8) + x1 #a__isLNat(x1) weight: 0 a__U56(x1) weight: 0 #a__U342(x1,x2,x3) weight: 0 a__U72(x1,x2) weight: 0 U334(x1,x2) weight: 0 #a__U101(x1,x2,x3) weight: 0 a__U11(x1,x2,x3) weight: 0 U32(x1,x2,x3) weight: 0 a__U53(x1,x2,x3) weight: 0 a__U141(x1) weight: (/ 1 4) a__U322(x1,x2,x3,x4) weight: 0 a__sel(x1,x2) weight: 0 a__U42(x1,x2,x3) weight: 0 a__U93(x1) weight: 0 U33(x1,x2,x3) weight: 0 #a__U45(x1,x2) weight: 0 a__U52(x1,x2,x3) weight: 0 a__U181(x1,x2) weight: 0 isLNatKind(x1) weight: (/ 1 4) + x1 U14(x1,x2,x3) weight: 0 U211(x1) weight: (/ 3 8) + x1 #a__U243(x1,x2,x3) weight: 0 #a__U54(x1,x2,x3) weight: 0 U203(x1,x2,x3) weight: 0 #a__U105(x1,x2) weight: 0 #a__U202(x1,x2,x3) weight: 0 a__U12(x1,x2,x3) weight: 0 U327(x1,x2) weight: 0 #a__U104(x1,x2,x3) weight: 0 #a__U201(x1,x2,x3) weight: 0 #a__U63(x1) weight: 0 a__isPLNat(x1) weight: 0 a__U327(x1,x2) weight: 0 U46(x1) weight: 0 #a__U332(x1,x2) weight: 0 a__U326(x1,x2,x3,x4) weight: 0 U251(x1,x2,x3) weight: 0 #a__U322(x1,x2,x3,x4) weight: 0 a__isLNatKind(x1) weight: (/ 1 8) #a__U121(x1,x2) weight: (/ 1 4) + x2 U52(x1,x2,x3) weight: 0 #a__U254(x1,x2,x3) weight: 0 #a__U324(x1,x2,x3,x4) weight: 0 #a__U281(x1,x2) weight: 0 #a__U251(x1,x2,x3) weight: 0 U61(x1,x2) weight: 0 a__U46(x1) weight: 0 #a__U22(x1,x2,x3) weight: 0 a__U13(x1,x2,x3) weight: 0 a__U304(x1,x2) weight: 0 U31(x1,x2,x3) weight: 0 #a__U83(x1) weight: 0 #a__U171(x1,x2) weight: (/ 1 4) + x2 a__U71(x1,x2) weight: 0 U183(x1) weight: 0 U245(x1,x2) weight: 0 U92(x1,x2) weight: 0 #a__isPLNat(x1) weight: 0 #a__U203(x1,x2,x3) weight: 0 head(x1) weight: (/ 1 8) + x1 #a__afterNth(x1,x2) weight: 0 U112(x1) weight: (/ 1 2) + x1 #a__U343(x1,x2,x3) weight: 0 #a__splitAt(x1,x2) weight: 0 #a__isPLNatKind(x1) weight: (/ 1 4) + x1 #a__U192(x1,x2) weight: 0 a__U255(x1,x2) weight: 0 cons(x1,x2) weight: (/ 1 4) + x1 + x2 a__U344(x1,x2,x3) weight: 0 a__U92(x1,x2) weight: 0 U323(x1,x2,x3,x4) weight: 0 a__U61(x1,x2) weight: 0 U102(x1,x2,x3) weight: 0 a__U105(x1,x2) weight: 0 a__U334(x1,x2) weight: 0 snd(x1) weight: (/ 1 4) + x1 a__take(x1,x2) weight: 0 U256(x1) weight: 0 a__U301(x1,x2,x3) weight: 0 U81(x1,x2) weight: 0 #a__U41(x1,x2,x3) weight: 0 U82(x1,x2) weight: 0 #a__U304(x1,x2) weight: 0 tt() weight: 0 a__isNatural(x1) weight: 0 a__isNaturalKind(x1) weight: (/ 1 8) a__U131(x1) weight: (/ 1 4) #a__isNatural(x1) weight: 0 U13(x1,x2,x3) weight: 0 #a__fst(x1) weight: 0 a__U23(x1,x2,x3) weight: 0 #a__U311(x1,x2) weight: 0 a__U201(x1,x2,x3) weight: 0 #a__U271(x1,x2) weight: (/ 1 4) + x2 a__U202(x1,x2,x3) weight: 0 U321(x1,x2,x3,x4) weight: 0 a__U282(x1,x2) weight: 0 #a__U241(x1,x2,x3) weight: 0 a__U183(x1) weight: 0 a__U333(x1,x2) weight: 0 U22(x1,x2,x3) weight: 0 #a__U293(x1,x2,x3) weight: 0 U51(x1,x2,x3) weight: 0 U311(x1,x2) weight: 0 #a__U325(x1,x2,x3,x4) weight: 0 #a__U34(x1,x2) weight: 0 U322(x1,x2,x3,x4) weight: 0 U344(x1,x2,x3) weight: 0 a__U342(x1,x2,x3) weight: 0 a__tail(x1) weight: 0 a__U103(x1,x2,x3) weight: 0 a__U54(x1,x2,x3) weight: 0 a__isPLNatKind(x1) weight: (/ 1 8) U53(x1,x2,x3) weight: 0 a__U303(x1,x2) weight: 0 a__U323(x1,x2,x3,x4) weight: 0 #a__U55(x1,x2) weight: 0 a__U112(x1) weight: (/ 3 8) #a__U331(x1,x2,x3) weight: 0 U41(x1,x2,x3) weight: 0 #a__tail(x1) weight: 0 a__U203(x1,x2,x3) weight: 0 #a__U32(x1,x2,x3) weight: 0 #a__U221(x1) weight: 0 a__U101(x1,x2,x3) weight: 0 #a__U91(x1,x2) weight: 0 a__U341(x1,x2,x3) weight: 0 U282(x1,x2) weight: 0 a__U256(x1) weight: 0 U121(x1,x2) weight: (/ 3 8) + x1 a__head(x1) weight: 0 U181(x1,x2) weight: 0 U324(x1,x2,x3,x4) weight: 0 U331(x1,x2,x3) weight: 0 U122(x1) weight: (/ 1 2) + x1 a__U312(x1,x2) weight: 0 #a__U327(x1,x2) weight: 0 Usable rules: { } Removed DPs: #63 #97 #98 #106 #129 #155 #193 #251 #252 #256 #260 #317 #349 #352 #353 #383 #386 #387 #437 #438 #450 #458 #459 Number of SCCs: 2, DPs: 298, edges: 25604 SCC { #1 #5 #7 #22 #30 #32 #48..51 #54 #74 #76 #110 #125 #126 #137 #144 #146 #159 #178 #180 #182 #184 #196 #201 #202 #212 #214 #223 #225 #233 #241 #242 #247 #250 #263 #280 #285 #298 #301..303 #308 #315 #344 #366 #408 #416 #424 #426 #433 #435 #460 #479 #485 #486 #490 #493 #494 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U291(x1,x2,x3) weight: 0 #a__U193(x1) weight: 0 a__U83(x1) weight: (/ 1 4) U231(x1,x2) weight: (/ 3 16) U301(x1,x2,x3) weight: 0 a__U293(x1,x2,x3) weight: 0 a__U241(x1,x2,x3) weight: (/ 1 8) + x3 U204(x1,x2,x3) weight: (/ 3 8) + x2 + x3 a__U324(x1,x2,x3,x4) weight: 0 a__U302(x1,x2) weight: 0 #a__isNaturalKind(x1) weight: 0 a__U325(x1,x2,x3,x4) weight: 0 a__U151(x1) weight: (/ 1 8) a__U292(x1,x2,x3) weight: 0 #a__U73(x1) weight: 0 #a__U131(x1) weight: 0 a__U63(x1) weight: (/ 3 16) U21(x1,x2,x3) weight: 0 U261(x1,x2) weight: (/ 3 16) + x2 a__U102(x1,x2,x3) weight: (/ 1 8) + x2 U254(x1,x2,x3) weight: (/ 1 4) + x2 U333(x1,x2) weight: 0 #a__U82(x1,x2) weight: (/ 1 16) + x2 a__U332(x1,x2) weight: 0 a__U45(x1,x2) weight: (/ 1 4) U193(x1) weight: (/ 1 2) + x1 #a__U72(x1,x2) weight: x2 #a__U242(x1,x2,x3) weight: x2 + x3 a__U246(x1) weight: (/ 5 16) U161(x1) weight: (/ 3 16) #a__U321(x1,x2,x3,x4) weight: 0 #a__U71(x1,x2) weight: x2 a__U232(x1) weight: (/ 3 16) U182(x1,x2) weight: (/ 1 8) + x2 #a__U291(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 a__U171(x1,x2) weight: (/ 1 8) #a__U92(x1,x2) weight: (/ 1 16) + x2 a__U104(x1,x2,x3) weight: (/ 3 16) a__U294(x1,x2,x3) weight: 0 a__U182(x1,x2) weight: (/ 1 16) + x1 a__U191(x1,x2) weight: (/ 5 16) a__U281(x1,x2) weight: 0 U243(x1,x2,x3) weight: (/ 1 4) + x2 + x3 a__U245(x1,x2) weight: (/ 1 4) #a__U112(x1) weight: 0 s(x1) weight: (/ 3 16) + x1 U105(x1,x2) weight: (/ 5 16) + x1 + x2 U303(x1,x2) weight: 0 #a__U292(x1,x2,x3) weight: 0 a__U24(x1,x2) weight: 0 #a__U341(x1,x2,x3) weight: 0 #a__U31(x1,x2,x3) weight: 0 a__U243(x1,x2,x3) weight: (/ 3 16) #a__U33(x1,x2,x3) weight: 0 #a__U93(x1) weight: 0 #a__head(x1) weight: 0 U192(x1,x2) weight: (/ 7 16) + x1 + x2 #a__U253(x1,x2,x3) weight: x2 + x3 U24(x1,x2) weight: 0 a__U33(x1,x2,x3) weight: 0 U106(x1) weight: (/ 3 8) + x1 #a__U24(x1,x2) weight: 0 #a__natsFrom(x1) weight: 0 isPLNatKind(x1) weight: (/ 1 8) #a__U252(x1,x2,x3) weight: x2 + x3 #a__U256(x1) weight: 0 a__U244(x1,x2,x3) weight: (/ 3 16) + x1 + x2 + x3 a__U343(x1,x2,x3) weight: 0 U242(x1,x2,x3) weight: (/ 3 16) + x2 + x3 #a__U303(x1,x2) weight: 0 U262(x1) weight: (/ 1 4) U244(x1,x2,x3) weight: (/ 1 4) U272(x1) weight: (/ 1 4) U56(x1) weight: (/ 1 4) #a__U191(x1,x2) weight: (/ 1 8) + x2 #a__U272(x1) weight: 0 #a__U23(x1,x2,x3) weight: 0 a__U55(x1,x2) weight: (/ 3 16) isPLNat(x1) weight: (/ 1 8) #a__snd(x1) weight: 0 a__U331(x1,x2,x3) weight: 0 #a__U312(x1,x2) weight: 0 a__afterNth(x1,x2) weight: 0 U42(x1,x2,x3) weight: (/ 1 8) + x2 + x3 U91(x1,x2) weight: (/ 3 16) + x2 U221(x1) weight: (/ 3 8) U293(x1,x2,x3) weight: 0 a__U73(x1) weight: (/ 1 8) #a__U106(x1) weight: 0 U325(x1,x2,x3,x4) weight: 0 a__U82(x1,x2) weight: (/ 3 16) #a__U182(x1,x2) weight: x2 take(x1,x2) weight: (/ 3 8) + x1 + x2 #a__U14(x1,x2,x3) weight: 0 U71(x1,x2) weight: (/ 1 8) + x2 a__U62(x1,x2) weight: (/ 1 8) + x1 a__U44(x1,x2,x3) weight: (/ 3 16) U131(x1) weight: (/ 3 16) + x1 U206(x1) weight: (/ 7 16) + x1 a__U221(x1) weight: (/ 5 16) U101(x1,x2,x3) weight: (/ 1 8) + x2 #a__U43(x1,x2,x3) weight: x2 + x3 #a__U334(x1,x2) weight: 0 pair(x1,x2) weight: x1 + x2 U255(x1,x2) weight: (/ 1 4) + x2 #a__U326(x1,x2,x3,x4) weight: 0 a__U261(x1,x2) weight: (/ 1 8) fst(x1) weight: x1 U111(x1,x2) weight: (/ 3 16) U43(x1,x2,x3) weight: (/ 3 16) + x1 + x2 + x3 #a__U13(x1,x2,x3) weight: 0 a__U121(x1,x2) weight: (/ 1 8) + x2 a__U262(x1) weight: (/ 3 16) #a__U246(x1) weight: 0 #a__U44(x1,x2,x3) weight: x2 + x3 #a__U204(x1,x2,x3) weight: x2 + x3 U103(x1,x2,x3) weight: (/ 3 16) + x2 + x3 a__U111(x1,x2) weight: (/ 1 8) a__U272(x1) weight: (/ 3 16) natsFrom(x1) weight: x1 U281(x1,x2) weight: 0 #a__U103(x1,x2,x3) weight: (/ 3 16) + x2 + x3 #a__U301(x1,x2,x3) weight: 0 U44(x1,x2,x3) weight: (/ 1 4) + x3 U55(x1,x2) weight: (/ 1 4) + x1 + x2 #a__U46(x1) weight: 0 a__snd(x1) weight: 0 a__U252(x1,x2,x3) weight: (/ 1 8) + x1 + x2 + x3 U253(x1,x2,x3) weight: (/ 1 4) + x1 U312(x1,x2) weight: 0 #a__U206(x1) weight: 0 #a__U181(x1,x2) weight: x2 a__U193(x1) weight: (/ 7 16) a__U271(x1,x2) weight: (/ 1 8) + x2 #a__U51(x1,x2,x3) weight: x2 + x3 U341(x1,x2,x3) weight: 0 a__U254(x1,x2,x3) weight: (/ 3 16) + x1 U23(x1,x2,x3) weight: 0 U292(x1,x2,x3) weight: 0 U342(x1,x2,x3) weight: 0 a__U172(x1) weight: (/ 3 16) U63(x1) weight: (/ 1 4) + x1 #a__U56(x1) weight: 0 #a__U344(x1,x2,x3) weight: 0 a__U22(x1,x2,x3) weight: 0 U172(x1) weight: (/ 1 4) + x1 U93(x1) weight: (/ 5 16) + x1 splitAt(x1,x2) weight: x1 + x2 isNaturalKind(x1) weight: (/ 1 8) U326(x1,x2,x3,x4) weight: 0 #a__U323(x1,x2,x3,x4) weight: 0 a__U106(x1) weight: (/ 5 16) U72(x1,x2) weight: (/ 1 8) #a__U11(x1,x2,x3) weight: 0 a__U291(x1,x2,x3) weight: 0 U241(x1,x2,x3) weight: (/ 3 16) + x1 U34(x1,x2) weight: 0 a__U192(x1,x2) weight: (/ 3 8) a__U31(x1,x2,x3) weight: 0 a__U51(x1,x2,x3) weight: (/ 1 16) + x1 + x2 + x3 a__U253(x1,x2,x3) weight: (/ 3 16) + x3 a__U81(x1,x2) weight: (/ 1 8) #a__U53(x1,x2,x3) weight: x2 + x3 #a__U205(x1,x2) weight: x2 #a__take(x1,x2) weight: 0 #a__U172(x1) weight: 0 #a__U255(x1,x2) weight: x2 U12(x1,x2,x3) weight: 0 a__U43(x1,x2,x3) weight: (/ 1 8) U271(x1,x2) weight: (/ 3 16) a__U231(x1,x2) weight: (/ 1 8) + x2 #a__U232(x1) weight: 0 #a__isLNatKind(x1) weight: (/ 1 16) #a__U62(x1,x2) weight: x2 a__U321(x1,x2,x3,x4) weight: 0 a__U206(x1) weight: (/ 3 8) isNatural(x1) weight: (/ 1 8) U302(x1,x2) weight: 0 U54(x1,x2,x3) weight: (/ 3 16) + x1 + x2 + x3 #a__U42(x1,x2,x3) weight: x2 + x3 #a__U183(x1) weight: 0 a__U41(x1,x2,x3) weight: (/ 1 16) + x1 + x3 U232(x1) weight: (/ 1 4) + x1 #a__U262(x1) weight: 0 #a__U122(x1) weight: 0 #a__U12(x1,x2,x3) weight: 0 U205(x1,x2) weight: (/ 3 8) a__U205(x1,x2) weight: (/ 5 16) + x1 + x2 U201(x1,x2,x3) weight: (/ 3 16) + x1 + x2 + x3 U104(x1,x2,x3) weight: (/ 1 4) + x1 + x2 + x3 a__U122(x1) weight: (/ 3 16) a__U14(x1,x2,x3) weight: 0 #a__U81(x1,x2) weight: (/ 1 8) + x2 #a__U21(x1,x2,x3) weight: 0 a__U161(x1) weight: (/ 1 8) #a__U61(x1,x2) weight: x2 #a__U333(x1,x2) weight: 0 a__U34(x1,x2) weight: 0 U252(x1,x2,x3) weight: (/ 3 16) #a__U261(x1,x2) weight: (/ 1 8) U141(x1) weight: (/ 3 16) + x1 a__fst(x1) weight: 0 tail(x1) weight: (/ 3 16) + x1 a__natsFrom(x1) weight: 0 #a__U302(x1,x2) weight: 0 U83(x1) weight: (/ 5 16) + x1 #a__U294(x1,x2,x3) weight: 0 #mark(x1) weight: 0 a__U204(x1,x2,x3) weight: (/ 5 16) 0() weight: 0 #a__U211(x1) weight: 0 U294(x1,x2,x3) weight: 0 #a__U244(x1,x2,x3) weight: x2 + x3 a__isLNat(x1) weight: (/ 1 16) U191(x1,x2) weight: (/ 3 8) + x1 + x2 U343(x1,x2,x3) weight: 0 a__U251(x1,x2,x3) weight: (/ 1 8) U73(x1) weight: (/ 3 16) + x1 #a__U282(x1,x2) weight: 0 a__U21(x1,x2,x3) weight: 0 U332(x1,x2) weight: 0 a__U311(x1,x2) weight: 0 U171(x1,x2) weight: (/ 3 16) + x2 a__U32(x1,x2,x3) weight: 0 a__U91(x1,x2) weight: (/ 1 8) #a__U231(x1,x2) weight: (/ 1 8) sel(x1,x2) weight: x1 + x2 U202(x1,x2,x3) weight: (/ 1 4) afterNth(x1,x2) weight: x1 + x2 #a__U151(x1) weight: 0 #a__U111(x1,x2) weight: (/ 1 8) #a__U161(x1) weight: 0 a__U242(x1,x2,x3) weight: (/ 1 8) + x1 #a__U141(x1) weight: 0 nil() weight: 0 a__splitAt(x1,x2) weight: 0 isLNat(x1) weight: (/ 1 8) + x1 U246(x1) weight: (/ 3 8) + x1 #a__U245(x1,x2) weight: x2 U62(x1,x2) weight: (/ 3 16) #a__U52(x1,x2,x3) weight: x2 + x3 a__U211(x1) weight: (/ 1 8) #a__U102(x1,x2,x3) weight: (/ 1 4) + x2 + x3 U304(x1,x2) weight: 0 U45(x1,x2) weight: (/ 5 16) + x1 + x2 #a__sel(x1,x2) weight: 0 mark(x1) weight: 0 U151(x1) weight: (/ 3 16) + x1 #a__isLNat(x1) weight: x1 a__U56(x1) weight: (/ 3 16) + x1 #a__U342(x1,x2,x3) weight: 0 a__U72(x1,x2) weight: (/ 1 16) + x1 U334(x1,x2) weight: 0 #a__U101(x1,x2,x3) weight: (/ 5 16) + x2 + x3 a__U11(x1,x2,x3) weight: 0 U32(x1,x2,x3) weight: 0 a__U53(x1,x2,x3) weight: (/ 1 16) + x1 + x2 + x3 a__U141(x1) weight: (/ 1 8) a__U322(x1,x2,x3,x4) weight: 0 a__sel(x1,x2) weight: 0 a__U42(x1,x2,x3) weight: (/ 1 16) + x1 a__U93(x1) weight: (/ 1 4) U33(x1,x2,x3) weight: 0 #a__U45(x1,x2) weight: x2 a__U52(x1,x2,x3) weight: (/ 1 16) + x1 a__U181(x1,x2) weight: (/ 1 16) + x1 isLNatKind(x1) weight: (/ 1 8) U14(x1,x2,x3) weight: 0 U211(x1) weight: (/ 3 16) + x1 #a__U243(x1,x2,x3) weight: x2 + x3 #a__U54(x1,x2,x3) weight: x2 + x3 U203(x1,x2,x3) weight: (/ 5 16) + x3 #a__U105(x1,x2) weight: (/ 1 16) + x2 #a__U202(x1,x2,x3) weight: x2 + x3 a__U12(x1,x2,x3) weight: 0 U327(x1,x2) weight: 0 #a__U104(x1,x2,x3) weight: (/ 1 8) + x2 + x3 #a__U201(x1,x2,x3) weight: x2 + x3 #a__U63(x1) weight: 0 a__isPLNat(x1) weight: (/ 1 16) + x1 a__U327(x1,x2) weight: 0 U46(x1) weight: (/ 3 8) + x1 #a__U332(x1,x2) weight: 0 a__U326(x1,x2,x3,x4) weight: 0 U251(x1,x2,x3) weight: (/ 3 16) #a__U322(x1,x2,x3,x4) weight: 0 a__isLNatKind(x1) weight: (/ 1 16) #a__U121(x1,x2) weight: (/ 1 8) U52(x1,x2,x3) weight: (/ 1 8) + x2 + x3 #a__U254(x1,x2,x3) weight: x2 + x3 #a__U324(x1,x2,x3,x4) weight: 0 #a__U281(x1,x2) weight: 0 #a__U251(x1,x2,x3) weight: x2 + x3 U61(x1,x2) weight: (/ 3 16) + x1 + x2 a__U46(x1) weight: (/ 5 16) #a__U22(x1,x2,x3) weight: 0 a__U13(x1,x2,x3) weight: 0 a__U304(x1,x2) weight: 0 U31(x1,x2,x3) weight: 0 #a__U83(x1) weight: 0 #a__U171(x1,x2) weight: (/ 1 8) a__U71(x1,x2) weight: (/ 1 16) + x1 U183(x1) weight: (/ 3 16) + x1 U245(x1,x2) weight: (/ 5 16) + x1 + x2 U92(x1,x2) weight: (/ 1 4) + x1 + x2 #a__isPLNat(x1) weight: x1 #a__U203(x1,x2,x3) weight: x2 + x3 head(x1) weight: x1 #a__afterNth(x1,x2) weight: 0 U112(x1) weight: (/ 1 4) + x1 #a__U343(x1,x2,x3) weight: 0 #a__splitAt(x1,x2) weight: 0 #a__isPLNatKind(x1) weight: (/ 1 8) #a__U192(x1,x2) weight: (/ 1 16) + x2 a__U255(x1,x2) weight: (/ 3 16) + x1 cons(x1,x2) weight: x1 + x2 a__U344(x1,x2,x3) weight: 0 a__U92(x1,x2) weight: (/ 3 16) U323(x1,x2,x3,x4) weight: 0 a__U61(x1,x2) weight: (/ 1 8) U102(x1,x2,x3) weight: (/ 3 16) + x3 a__U105(x1,x2) weight: (/ 1 4) a__U334(x1,x2) weight: 0 snd(x1) weight: (/ 3 16) + x1 a__take(x1,x2) weight: 0 U256(x1) weight: (/ 5 16) + x1 a__U301(x1,x2,x3) weight: 0 U81(x1,x2) weight: (/ 3 16) + x1 + x2 #a__U41(x1,x2,x3) weight: x2 + x3 U82(x1,x2) weight: (/ 1 4) + x1 + x2 #a__U304(x1,x2) weight: 0 tt() weight: 0 a__isNatural(x1) weight: (/ 1 16) + x1 a__isNaturalKind(x1) weight: (/ 1 16) + x1 a__U131(x1) weight: (/ 1 8) #a__isNatural(x1) weight: x1 U13(x1,x2,x3) weight: 0 #a__fst(x1) weight: 0 a__U23(x1,x2,x3) weight: 0 #a__U311(x1,x2) weight: 0 a__U201(x1,x2,x3) weight: (/ 1 8) #a__U271(x1,x2) weight: (/ 1 8) a__U202(x1,x2,x3) weight: (/ 3 16) + x3 U321(x1,x2,x3,x4) weight: 0 a__U282(x1,x2) weight: 0 #a__U241(x1,x2,x3) weight: x2 + x3 a__U183(x1) weight: (/ 1 8) a__U333(x1,x2) weight: 0 U22(x1,x2,x3) weight: 0 #a__U293(x1,x2,x3) weight: 0 U51(x1,x2,x3) weight: (/ 1 8) U311(x1,x2) weight: 0 #a__U325(x1,x2,x3,x4) weight: 0 #a__U34(x1,x2) weight: 0 U322(x1,x2,x3,x4) weight: 0 U344(x1,x2,x3) weight: 0 a__U342(x1,x2,x3) weight: 0 a__tail(x1) weight: 0 a__U103(x1,x2,x3) weight: (/ 1 8) + x1 a__U54(x1,x2,x3) weight: (/ 1 8) a__isPLNatKind(x1) weight: (/ 1 16) U53(x1,x2,x3) weight: (/ 1 8) a__U303(x1,x2) weight: 0 a__U323(x1,x2,x3,x4) weight: 0 #a__U55(x1,x2) weight: x2 a__U112(x1) weight: (/ 3 16) #a__U331(x1,x2,x3) weight: 0 U41(x1,x2,x3) weight: (/ 1 8) + x2 #a__tail(x1) weight: 0 a__U203(x1,x2,x3) weight: (/ 1 4) + x2 #a__U32(x1,x2,x3) weight: 0 #a__U221(x1) weight: 0 a__U101(x1,x2,x3) weight: (/ 1 16) + x1 + x3 #a__U91(x1,x2) weight: (/ 1 8) + x2 a__U341(x1,x2,x3) weight: 0 U282(x1,x2) weight: 0 a__U256(x1) weight: (/ 1 4) U121(x1,x2) weight: (/ 3 16) + x1 a__head(x1) weight: 0 U181(x1,x2) weight: (/ 1 8) + x2 U324(x1,x2,x3,x4) weight: 0 U331(x1,x2,x3) weight: 0 U122(x1) weight: (/ 1 4) + x1 a__U312(x1,x2) weight: 0 #a__U327(x1,x2) weight: 0 Usable rules: { } Removed DPs: #1 #125 #144 #178 #182 #225 #233 #250 #298 #301 #416 #426 #433 #460 #485 #486 Number of SCCs: 2, DPs: 282, edges: 25544 SCC { #5 #7 #22 #30 #32 #48..51 #54 #74 #76 #110 #126 #137 #146 #159 #180 #184 #196 #201 #202 #212 #214 #223 #241 #242 #247 #263 #280 #285 #302 #303 #308 #315 #344 #366 #408 #424 #435 #479 #490 #493 #494 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U291(x1,x2,x3) weight: 0 #a__U193(x1) weight: 0 a__U83(x1) weight: (/ 1 4) U231(x1,x2) weight: (/ 3 16) U301(x1,x2,x3) weight: 0 a__U293(x1,x2,x3) weight: 0 a__U241(x1,x2,x3) weight: (/ 3 16) + x3 U204(x1,x2,x3) weight: (/ 1 16) a__U324(x1,x2,x3,x4) weight: 0 a__U302(x1,x2) weight: 0 #a__isNaturalKind(x1) weight: 0 a__U325(x1,x2,x3,x4) weight: 0 a__U151(x1) weight: (/ 1 8) a__U292(x1,x2,x3) weight: 0 #a__U73(x1) weight: 0 #a__U131(x1) weight: 0 a__U63(x1) weight: (/ 3 16) U21(x1,x2,x3) weight: 0 U261(x1,x2) weight: (/ 3 16) + x2 a__U102(x1,x2,x3) weight: (/ 1 8) + x2 U254(x1,x2,x3) weight: (/ 1 4) + x2 U333(x1,x2) weight: 0 #a__U82(x1,x2) weight: (/ 1 16) a__U332(x1,x2) weight: 0 a__U45(x1,x2) weight: (/ 1 4) U193(x1) weight: (/ 1 4) #a__U72(x1,x2) weight: (/ 1 4) + x2 #a__U242(x1,x2,x3) weight: (/ 1 4) + x2 + x3 a__U246(x1) weight: (/ 3 8) U161(x1) weight: (/ 3 16) #a__U321(x1,x2,x3,x4) weight: 0 #a__U71(x1,x2) weight: (/ 5 16) + x2 a__U232(x1) weight: (/ 3 16) U182(x1,x2) weight: 0 #a__U291(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 a__U171(x1,x2) weight: (/ 1 8) #a__U92(x1,x2) weight: (/ 1 16) a__U104(x1,x2,x3) weight: (/ 3 16) a__U294(x1,x2,x3) weight: 0 a__U182(x1,x2) weight: 0 a__U191(x1,x2) weight: (/ 1 4) a__U281(x1,x2) weight: 0 U243(x1,x2,x3) weight: (/ 5 16) + x2 + x3 a__U245(x1,x2) weight: (/ 5 16) #a__U112(x1) weight: 0 s(x1) weight: (/ 3 16) + x1 U105(x1,x2) weight: (/ 5 16) + x1 + x2 U303(x1,x2) weight: 0 #a__U292(x1,x2,x3) weight: 0 a__U24(x1,x2) weight: 0 #a__U341(x1,x2,x3) weight: 0 #a__U31(x1,x2,x3) weight: 0 a__U243(x1,x2,x3) weight: (/ 1 4) #a__U33(x1,x2,x3) weight: 0 #a__U93(x1) weight: 0 #a__head(x1) weight: 0 U192(x1,x2) weight: (/ 1 4) #a__U253(x1,x2,x3) weight: (/ 5 16) + x2 + x3 U24(x1,x2) weight: 0 a__U33(x1,x2,x3) weight: 0 U106(x1) weight: (/ 3 8) + x1 #a__U24(x1,x2) weight: 0 #a__natsFrom(x1) weight: 0 isPLNatKind(x1) weight: (/ 1 8) #a__U252(x1,x2,x3) weight: (/ 3 8) + x2 + x3 #a__U256(x1) weight: 0 a__U244(x1,x2,x3) weight: (/ 1 4) + x1 + x2 + x3 a__U343(x1,x2,x3) weight: 0 U242(x1,x2,x3) weight: (/ 1 4) + x2 + x3 #a__U303(x1,x2) weight: 0 U262(x1) weight: (/ 1 4) U244(x1,x2,x3) weight: (/ 5 16) U272(x1) weight: (/ 1 4) U56(x1) weight: (/ 1 4) #a__U191(x1,x2) weight: (/ 1 8) #a__U272(x1) weight: 0 #a__U23(x1,x2,x3) weight: 0 a__U55(x1,x2) weight: (/ 3 16) isPLNat(x1) weight: (/ 1 8) #a__snd(x1) weight: 0 a__U331(x1,x2,x3) weight: 0 #a__U312(x1,x2) weight: 0 a__afterNth(x1,x2) weight: 0 U42(x1,x2,x3) weight: (/ 1 8) + x2 + x3 U91(x1,x2) weight: (/ 3 16) + x2 U221(x1) weight: (/ 3 8) U293(x1,x2,x3) weight: 0 a__U73(x1) weight: (/ 1 8) #a__U106(x1) weight: 0 U325(x1,x2,x3,x4) weight: 0 a__U82(x1,x2) weight: (/ 3 16) #a__U182(x1,x2) weight: (/ 1 16) + x2 take(x1,x2) weight: (/ 3 8) + x1 + x2 #a__U14(x1,x2,x3) weight: 0 U71(x1,x2) weight: (/ 1 8) + x2 a__U62(x1,x2) weight: (/ 1 8) + x1 a__U44(x1,x2,x3) weight: (/ 3 16) U131(x1) weight: (/ 3 16) + x1 U206(x1) weight: (/ 1 16) a__U221(x1) weight: (/ 5 16) U101(x1,x2,x3) weight: (/ 1 8) + x2 #a__U43(x1,x2,x3) weight: (/ 5 16) + x2 + x3 #a__U334(x1,x2) weight: 0 pair(x1,x2) weight: (/ 1 16) + x1 + x2 U255(x1,x2) weight: (/ 1 4) + x2 #a__U326(x1,x2,x3,x4) weight: 0 a__U261(x1,x2) weight: (/ 1 8) fst(x1) weight: (/ 11 16) + x1 U111(x1,x2) weight: (/ 3 16) U43(x1,x2,x3) weight: (/ 3 16) + x1 + x2 + x3 #a__U13(x1,x2,x3) weight: 0 a__U121(x1,x2) weight: (/ 1 8) + x2 a__U262(x1) weight: (/ 3 16) #a__U246(x1) weight: 0 #a__U44(x1,x2,x3) weight: (/ 1 4) + x2 + x3 #a__U204(x1,x2,x3) weight: (/ 3 16) + x2 + x3 U103(x1,x2,x3) weight: (/ 3 16) + x2 + x3 a__U111(x1,x2) weight: (/ 1 8) a__U272(x1) weight: (/ 3 16) natsFrom(x1) weight: (/ 3 8) + x1 U281(x1,x2) weight: 0 #a__U103(x1,x2,x3) weight: (/ 3 16) #a__U301(x1,x2,x3) weight: 0 U44(x1,x2,x3) weight: (/ 1 4) + x3 U55(x1,x2) weight: (/ 1 4) + x1 + x2 #a__U46(x1) weight: 0 a__snd(x1) weight: 0 a__U252(x1,x2,x3) weight: (/ 1 8) + x1 + x2 + x3 U253(x1,x2,x3) weight: (/ 1 4) + x1 U312(x1,x2) weight: 0 #a__U206(x1) weight: 0 #a__U181(x1,x2) weight: (/ 1 8) + x2 a__U193(x1) weight: (/ 1 4) a__U271(x1,x2) weight: (/ 1 8) + x2 #a__U51(x1,x2,x3) weight: (/ 7 16) + x2 + x3 U341(x1,x2,x3) weight: 0 a__U254(x1,x2,x3) weight: (/ 3 16) + x1 U23(x1,x2,x3) weight: 0 U292(x1,x2,x3) weight: 0 U342(x1,x2,x3) weight: 0 a__U172(x1) weight: (/ 3 16) U63(x1) weight: (/ 1 4) + x1 #a__U56(x1) weight: 0 #a__U344(x1,x2,x3) weight: 0 a__U22(x1,x2,x3) weight: 0 U172(x1) weight: (/ 1 4) + x1 U93(x1) weight: (/ 5 16) + x1 splitAt(x1,x2) weight: x1 + x2 isNaturalKind(x1) weight: (/ 1 8) U326(x1,x2,x3,x4) weight: 0 #a__U323(x1,x2,x3,x4) weight: 0 a__U106(x1) weight: (/ 5 16) U72(x1,x2) weight: (/ 1 8) #a__U11(x1,x2,x3) weight: 0 a__U291(x1,x2,x3) weight: 0 U241(x1,x2,x3) weight: (/ 1 4) + x1 U34(x1,x2) weight: 0 a__U192(x1,x2) weight: (/ 1 4) a__U31(x1,x2,x3) weight: 0 a__U51(x1,x2,x3) weight: (/ 1 16) + x1 + x2 + x3 a__U253(x1,x2,x3) weight: (/ 3 16) + x3 a__U81(x1,x2) weight: (/ 1 8) #a__U53(x1,x2,x3) weight: (/ 5 16) + x2 + x3 #a__U205(x1,x2) weight: (/ 1 16) + x1 + x2 #a__take(x1,x2) weight: 0 #a__U172(x1) weight: 0 #a__U255(x1,x2) weight: (/ 1 16) + x1 + x2 U12(x1,x2,x3) weight: 0 a__U43(x1,x2,x3) weight: (/ 1 8) U271(x1,x2) weight: (/ 3 16) a__U231(x1,x2) weight: (/ 1 8) + x2 #a__U232(x1) weight: 0 #a__isLNatKind(x1) weight: (/ 1 16) #a__U62(x1,x2) weight: (/ 9 16) + x2 a__U321(x1,x2,x3,x4) weight: 0 a__U206(x1) weight: (/ 1 16) isNatural(x1) weight: (/ 1 16) U302(x1,x2) weight: 0 U54(x1,x2,x3) weight: (/ 3 16) + x1 + x2 + x3 #a__U42(x1,x2,x3) weight: (/ 3 8) + x2 + x3 #a__U183(x1) weight: 0 a__U41(x1,x2,x3) weight: (/ 1 16) + x1 + x3 U232(x1) weight: (/ 1 4) + x1 #a__U262(x1) weight: 0 #a__U122(x1) weight: 0 #a__U12(x1,x2,x3) weight: 0 U205(x1,x2) weight: (/ 1 16) a__U205(x1,x2) weight: (/ 1 16) U201(x1,x2,x3) weight: (/ 1 16) U104(x1,x2,x3) weight: (/ 1 4) + x1 + x2 + x3 a__U122(x1) weight: (/ 3 16) a__U14(x1,x2,x3) weight: 0 #a__U81(x1,x2) weight: (/ 1 8) #a__U21(x1,x2,x3) weight: 0 a__U161(x1) weight: (/ 1 8) #a__U61(x1,x2) weight: (/ 5 8) + x2 #a__U333(x1,x2) weight: 0 a__U34(x1,x2) weight: 0 U252(x1,x2,x3) weight: (/ 3 16) #a__U261(x1,x2) weight: (/ 1 8) U141(x1) weight: (/ 3 16) + x1 a__fst(x1) weight: 0 tail(x1) weight: (/ 3 16) + x1 a__natsFrom(x1) weight: 0 #a__U302(x1,x2) weight: 0 U83(x1) weight: (/ 5 16) + x1 #a__U294(x1,x2,x3) weight: 0 #mark(x1) weight: 0 a__U204(x1,x2,x3) weight: (/ 1 16) 0() weight: 0 #a__U211(x1) weight: 0 U294(x1,x2,x3) weight: 0 #a__U244(x1,x2,x3) weight: (/ 1 8) + x2 + x3 a__isLNat(x1) weight: (/ 1 16) U191(x1,x2) weight: (/ 1 4) U343(x1,x2,x3) weight: 0 a__U251(x1,x2,x3) weight: (/ 1 8) U73(x1) weight: (/ 3 16) + x1 #a__U282(x1,x2) weight: 0 a__U21(x1,x2,x3) weight: 0 U332(x1,x2) weight: 0 a__U311(x1,x2) weight: 0 U171(x1,x2) weight: (/ 3 16) + x2 a__U32(x1,x2,x3) weight: 0 a__U91(x1,x2) weight: (/ 1 8) #a__U231(x1,x2) weight: (/ 1 8) sel(x1,x2) weight: x1 + x2 U202(x1,x2,x3) weight: (/ 1 16) afterNth(x1,x2) weight: (/ 1 2) + x1 + x2 #a__U151(x1) weight: 0 #a__U111(x1,x2) weight: (/ 1 8) #a__U161(x1) weight: 0 a__U242(x1,x2,x3) weight: (/ 3 16) + x1 #a__U141(x1) weight: 0 nil() weight: 0 a__splitAt(x1,x2) weight: 0 isLNat(x1) weight: (/ 1 8) + x1 U246(x1) weight: (/ 7 16) + x1 #a__U245(x1,x2) weight: (/ 1 16) + x2 U62(x1,x2) weight: (/ 3 16) #a__U52(x1,x2,x3) weight: (/ 3 8) + x2 + x3 a__U211(x1) weight: (/ 3 16) #a__U102(x1,x2,x3) weight: (/ 1 4) U304(x1,x2) weight: 0 U45(x1,x2) weight: (/ 5 16) + x1 + x2 #a__sel(x1,x2) weight: 0 mark(x1) weight: 0 U151(x1) weight: (/ 3 16) + x1 #a__isLNat(x1) weight: x1 a__U56(x1) weight: (/ 3 16) + x1 #a__U342(x1,x2,x3) weight: 0 a__U72(x1,x2) weight: (/ 1 16) + x1 U334(x1,x2) weight: 0 #a__U101(x1,x2,x3) weight: (/ 5 16) a__U11(x1,x2,x3) weight: 0 U32(x1,x2,x3) weight: 0 a__U53(x1,x2,x3) weight: (/ 1 16) + x1 + x2 + x3 a__U141(x1) weight: (/ 1 8) a__U322(x1,x2,x3,x4) weight: 0 a__sel(x1,x2) weight: 0 a__U42(x1,x2,x3) weight: (/ 1 16) + x1 a__U93(x1) weight: (/ 1 4) U33(x1,x2,x3) weight: 0 #a__U45(x1,x2) weight: (/ 1 16) + x2 a__U52(x1,x2,x3) weight: (/ 1 16) + x1 a__U181(x1,x2) weight: (/ 1 8) isLNatKind(x1) weight: (/ 1 8) U14(x1,x2,x3) weight: 0 U211(x1) weight: (/ 1 4) + x1 #a__U243(x1,x2,x3) weight: (/ 3 16) + x2 + x3 #a__U54(x1,x2,x3) weight: (/ 1 4) + x2 + x3 U203(x1,x2,x3) weight: (/ 1 16) #a__U105(x1,x2) weight: (/ 1 16) #a__U202(x1,x2,x3) weight: (/ 3 16) + x2 + x3 a__U12(x1,x2,x3) weight: 0 U327(x1,x2) weight: 0 #a__U104(x1,x2,x3) weight: (/ 1 8) #a__U201(x1,x2,x3) weight: (/ 3 16) + x2 + x3 #a__U63(x1) weight: 0 a__isPLNat(x1) weight: (/ 1 16) + x1 a__U327(x1,x2) weight: 0 U46(x1) weight: (/ 3 8) + x1 #a__U332(x1,x2) weight: 0 a__U326(x1,x2,x3,x4) weight: 0 U251(x1,x2,x3) weight: (/ 3 16) #a__U322(x1,x2,x3,x4) weight: 0 a__isLNatKind(x1) weight: (/ 1 16) #a__U121(x1,x2) weight: (/ 1 8) U52(x1,x2,x3) weight: (/ 1 8) + x2 + x3 #a__U254(x1,x2,x3) weight: (/ 1 4) + x2 + x3 #a__U324(x1,x2,x3,x4) weight: 0 #a__U281(x1,x2) weight: 0 #a__U251(x1,x2,x3) weight: (/ 7 16) + x2 + x3 U61(x1,x2) weight: (/ 3 16) + x1 + x2 a__U46(x1) weight: (/ 5 16) #a__U22(x1,x2,x3) weight: 0 a__U13(x1,x2,x3) weight: 0 a__U304(x1,x2) weight: 0 U31(x1,x2,x3) weight: 0 #a__U83(x1) weight: 0 #a__U171(x1,x2) weight: (/ 1 8) a__U71(x1,x2) weight: (/ 1 16) + x1 U183(x1) weight: 0 U245(x1,x2) weight: (/ 3 8) + x1 + x2 U92(x1,x2) weight: (/ 1 4) + x1 + x2 #a__isPLNat(x1) weight: (/ 1 2) + x1 #a__U203(x1,x2,x3) weight: (/ 3 16) + x2 + x3 head(x1) weight: (/ 1 16) + x1 #a__afterNth(x1,x2) weight: 0 U112(x1) weight: (/ 1 4) + x1 #a__U343(x1,x2,x3) weight: 0 #a__splitAt(x1,x2) weight: 0 #a__isPLNatKind(x1) weight: (/ 1 8) #a__U192(x1,x2) weight: (/ 1 16) a__U255(x1,x2) weight: (/ 3 16) + x1 cons(x1,x2) weight: (/ 1 2) + x1 + x2 a__U344(x1,x2,x3) weight: 0 a__U92(x1,x2) weight: (/ 3 16) U323(x1,x2,x3,x4) weight: 0 a__U61(x1,x2) weight: (/ 1 8) U102(x1,x2,x3) weight: (/ 3 16) + x3 a__U105(x1,x2) weight: (/ 1 4) a__U334(x1,x2) weight: 0 snd(x1) weight: (/ 3 16) + x1 a__take(x1,x2) weight: 0 U256(x1) weight: (/ 5 16) + x1 a__U301(x1,x2,x3) weight: 0 U81(x1,x2) weight: (/ 3 16) + x1 + x2 #a__U41(x1,x2,x3) weight: (/ 7 16) + x2 + x3 U82(x1,x2) weight: (/ 1 4) + x1 + x2 #a__U304(x1,x2) weight: 0 tt() weight: 0 a__isNatural(x1) weight: (/ 1 16) + x1 a__isNaturalKind(x1) weight: (/ 1 16) + x1 a__U131(x1) weight: (/ 1 8) #a__isNatural(x1) weight: (/ 3 16) + x1 U13(x1,x2,x3) weight: 0 #a__fst(x1) weight: 0 a__U23(x1,x2,x3) weight: 0 #a__U311(x1,x2) weight: 0 a__U201(x1,x2,x3) weight: (/ 1 16) #a__U271(x1,x2) weight: (/ 1 8) a__U202(x1,x2,x3) weight: (/ 1 16) U321(x1,x2,x3,x4) weight: 0 a__U282(x1,x2) weight: 0 #a__U241(x1,x2,x3) weight: (/ 5 16) + x2 + x3 a__U183(x1) weight: 0 a__U333(x1,x2) weight: 0 U22(x1,x2,x3) weight: 0 #a__U293(x1,x2,x3) weight: 0 U51(x1,x2,x3) weight: (/ 1 8) U311(x1,x2) weight: 0 #a__U325(x1,x2,x3,x4) weight: 0 #a__U34(x1,x2) weight: 0 U322(x1,x2,x3,x4) weight: 0 U344(x1,x2,x3) weight: 0 a__U342(x1,x2,x3) weight: 0 a__tail(x1) weight: 0 a__U103(x1,x2,x3) weight: (/ 1 8) + x1 a__U54(x1,x2,x3) weight: (/ 1 8) a__isPLNatKind(x1) weight: (/ 1 16) U53(x1,x2,x3) weight: (/ 1 8) a__U303(x1,x2) weight: 0 a__U323(x1,x2,x3,x4) weight: 0 #a__U55(x1,x2) weight: (/ 1 16) + x2 a__U112(x1) weight: (/ 3 16) #a__U331(x1,x2,x3) weight: 0 U41(x1,x2,x3) weight: (/ 1 8) + x2 #a__tail(x1) weight: 0 a__U203(x1,x2,x3) weight: (/ 1 16) #a__U32(x1,x2,x3) weight: 0 #a__U221(x1) weight: 0 a__U101(x1,x2,x3) weight: (/ 1 16) + x1 + x3 #a__U91(x1,x2) weight: (/ 1 8) a__U341(x1,x2,x3) weight: 0 U282(x1,x2) weight: 0 a__U256(x1) weight: (/ 1 4) U121(x1,x2) weight: (/ 3 16) + x1 a__head(x1) weight: 0 U181(x1,x2) weight: (/ 1 8) U324(x1,x2,x3,x4) weight: 0 U331(x1,x2,x3) weight: 0 U122(x1) weight: (/ 1 4) + x1 a__U312(x1,x2) weight: 0 #a__U327(x1,x2) weight: 0 Usable rules: { 21..32 131..134 289 308..319 } Removed DPs: #5 #22 #30 #32 #48..51 #54 #74 #76 #110 #126 #137 #146 #159 #180 #196 #201 #202 #212 #214 #223 #241 #247 #263 #280 #285 #302 #303 #315 #366 #408 #424 #435 #479 #490 #493 #494 Number of SCCs: 2, DPs: 243, edges: 25473 SCC { #7 #184 #242 #308 #344 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U291(x1,x2,x3) weight: 0 #a__U193(x1) weight: 0 a__U83(x1) weight: (/ 1 4) U231(x1,x2) weight: (/ 3 16) U301(x1,x2,x3) weight: 0 a__U293(x1,x2,x3) weight: 0 a__U241(x1,x2,x3) weight: (/ 3 16) + x3 U204(x1,x2,x3) weight: (/ 3 8) a__U324(x1,x2,x3,x4) weight: 0 a__U302(x1,x2) weight: 0 #a__isNaturalKind(x1) weight: 0 a__U325(x1,x2,x3,x4) weight: 0 a__U151(x1) weight: (/ 1 8) a__U292(x1,x2,x3) weight: 0 #a__U73(x1) weight: 0 #a__U131(x1) weight: 0 a__U63(x1) weight: (/ 3 16) U21(x1,x2,x3) weight: 0 U261(x1,x2) weight: (/ 3 16) + x2 a__U102(x1,x2,x3) weight: (/ 1 8) U254(x1,x2,x3) weight: (/ 1 4) + x2 U333(x1,x2) weight: 0 #a__U82(x1,x2) weight: (/ 1 16) a__U332(x1,x2) weight: 0 a__U45(x1,x2) weight: (/ 1 4) U193(x1) weight: (/ 1 8) #a__U72(x1,x2) weight: (/ 1 4) #a__U242(x1,x2,x3) weight: (/ 1 4) a__U246(x1) weight: (/ 3 8) U161(x1) weight: (/ 3 16) #a__U321(x1,x2,x3,x4) weight: 0 #a__U71(x1,x2) weight: (/ 5 16) a__U232(x1) weight: (/ 3 16) U182(x1,x2) weight: 0 #a__U291(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 a__U171(x1,x2) weight: (/ 1 8) #a__U92(x1,x2) weight: (/ 1 16) a__U104(x1,x2,x3) weight: (/ 3 16) a__U294(x1,x2,x3) weight: 0 a__U182(x1,x2) weight: 0 a__U191(x1,x2) weight: (/ 1 8) a__U281(x1,x2) weight: 0 U243(x1,x2,x3) weight: (/ 5 16) + x2 + x3 a__U245(x1,x2) weight: (/ 5 16) #a__U112(x1) weight: 0 s(x1) weight: (/ 1 16) + x1 U105(x1,x2) weight: (/ 5 16) + x1 + x2 U303(x1,x2) weight: 0 #a__U292(x1,x2,x3) weight: 0 a__U24(x1,x2) weight: 0 #a__U341(x1,x2,x3) weight: 0 #a__U31(x1,x2,x3) weight: 0 a__U243(x1,x2,x3) weight: (/ 1 4) #a__U33(x1,x2,x3) weight: 0 #a__U93(x1) weight: 0 #a__head(x1) weight: 0 U192(x1,x2) weight: (/ 1 8) #a__U253(x1,x2,x3) weight: (/ 5 16) U24(x1,x2) weight: 0 a__U33(x1,x2,x3) weight: 0 U106(x1) weight: (/ 3 8) + x1 #a__U24(x1,x2) weight: 0 #a__natsFrom(x1) weight: 0 isPLNatKind(x1) weight: (/ 1 8) #a__U252(x1,x2,x3) weight: (/ 3 8) #a__U256(x1) weight: 0 a__U244(x1,x2,x3) weight: (/ 1 4) + x1 + x2 + x3 a__U343(x1,x2,x3) weight: 0 U242(x1,x2,x3) weight: (/ 1 4) + x2 + x3 #a__U303(x1,x2) weight: 0 U262(x1) weight: (/ 1 4) U244(x1,x2,x3) weight: (/ 5 16) U272(x1) weight: (/ 1 4) U56(x1) weight: (/ 1 4) #a__U191(x1,x2) weight: (/ 1 8) #a__U272(x1) weight: 0 #a__U23(x1,x2,x3) weight: 0 a__U55(x1,x2) weight: (/ 3 16) isPLNat(x1) weight: (/ 1 8) #a__snd(x1) weight: 0 a__U331(x1,x2,x3) weight: 0 #a__U312(x1,x2) weight: 0 a__afterNth(x1,x2) weight: 0 U42(x1,x2,x3) weight: (/ 1 8) + x2 + x3 U91(x1,x2) weight: (/ 3 16) + x2 U221(x1) weight: (/ 3 16) U293(x1,x2,x3) weight: 0 a__U73(x1) weight: (/ 1 8) #a__U106(x1) weight: 0 U325(x1,x2,x3,x4) weight: 0 a__U82(x1,x2) weight: (/ 3 16) #a__U182(x1,x2) weight: (/ 1 16) take(x1,x2) weight: (/ 3 8) + x1 + x2 #a__U14(x1,x2,x3) weight: 0 U71(x1,x2) weight: (/ 1 8) + x2 a__U62(x1,x2) weight: (/ 1 8) + x1 a__U44(x1,x2,x3) weight: (/ 3 16) U131(x1) weight: (/ 3 16) + x1 U206(x1) weight: (/ 3 8) a__U221(x1) weight: (/ 1 8) U101(x1,x2,x3) weight: (/ 1 8) + x2 #a__U43(x1,x2,x3) weight: (/ 5 16) #a__U334(x1,x2) weight: 0 pair(x1,x2) weight: (/ 1 16) + x1 + x2 U255(x1,x2) weight: (/ 1 4) + x2 #a__U326(x1,x2,x3,x4) weight: 0 a__U261(x1,x2) weight: (/ 1 8) fst(x1) weight: (/ 11 16) + x1 U111(x1,x2) weight: (/ 3 16) U43(x1,x2,x3) weight: (/ 3 16) + x1 + x2 + x3 #a__U13(x1,x2,x3) weight: 0 a__U121(x1,x2) weight: (/ 1 8) + x2 a__U262(x1) weight: (/ 3 16) #a__U246(x1) weight: 0 #a__U44(x1,x2,x3) weight: (/ 1 4) #a__U204(x1,x2,x3) weight: (/ 1 16) + x2 U103(x1,x2,x3) weight: (/ 3 16) + x2 + x3 a__U111(x1,x2) weight: (/ 1 8) a__U272(x1) weight: (/ 3 16) natsFrom(x1) weight: (/ 3 8) + x1 U281(x1,x2) weight: 0 #a__U103(x1,x2,x3) weight: (/ 3 16) #a__U301(x1,x2,x3) weight: 0 U44(x1,x2,x3) weight: (/ 1 4) + x3 U55(x1,x2) weight: (/ 1 4) + x1 + x2 #a__U46(x1) weight: 0 a__snd(x1) weight: 0 a__U252(x1,x2,x3) weight: (/ 1 8) + x1 + x2 + x3 U253(x1,x2,x3) weight: (/ 1 4) + x1 U312(x1,x2) weight: 0 #a__U206(x1) weight: 0 #a__U181(x1,x2) weight: (/ 1 8) a__U193(x1) weight: (/ 1 8) a__U271(x1,x2) weight: (/ 1 8) + x2 #a__U51(x1,x2,x3) weight: (/ 7 16) U341(x1,x2,x3) weight: 0 a__U254(x1,x2,x3) weight: (/ 3 16) + x1 U23(x1,x2,x3) weight: 0 U292(x1,x2,x3) weight: 0 U342(x1,x2,x3) weight: 0 a__U172(x1) weight: (/ 3 16) U63(x1) weight: (/ 1 4) + x1 #a__U56(x1) weight: 0 #a__U344(x1,x2,x3) weight: 0 a__U22(x1,x2,x3) weight: 0 U172(x1) weight: (/ 1 4) + x1 U93(x1) weight: (/ 5 16) + x1 splitAt(x1,x2) weight: x1 + x2 isNaturalKind(x1) weight: (/ 1 8) U326(x1,x2,x3,x4) weight: 0 #a__U323(x1,x2,x3,x4) weight: 0 a__U106(x1) weight: (/ 5 16) U72(x1,x2) weight: (/ 1 8) #a__U11(x1,x2,x3) weight: 0 a__U291(x1,x2,x3) weight: 0 U241(x1,x2,x3) weight: (/ 1 4) + x1 U34(x1,x2) weight: 0 a__U192(x1,x2) weight: (/ 1 8) a__U31(x1,x2,x3) weight: 0 a__U51(x1,x2,x3) weight: (/ 1 16) + x1 + x2 + x3 a__U253(x1,x2,x3) weight: (/ 3 16) + x3 a__U81(x1,x2) weight: (/ 1 8) #a__U53(x1,x2,x3) weight: (/ 5 16) #a__U205(x1,x2) weight: (/ 1 16) + x1 #a__take(x1,x2) weight: 0 #a__U172(x1) weight: 0 #a__U255(x1,x2) weight: (/ 1 16) + x1 U12(x1,x2,x3) weight: 0 a__U43(x1,x2,x3) weight: (/ 1 8) U271(x1,x2) weight: (/ 3 16) a__U231(x1,x2) weight: (/ 1 8) #a__U232(x1) weight: 0 #a__isLNatKind(x1) weight: (/ 1 16) #a__U62(x1,x2) weight: (/ 9 16) a__U321(x1,x2,x3,x4) weight: 0 a__U206(x1) weight: (/ 3 8) isNatural(x1) weight: (/ 1 16) U302(x1,x2) weight: 0 U54(x1,x2,x3) weight: (/ 3 16) + x1 + x2 + x3 #a__U42(x1,x2,x3) weight: (/ 3 8) #a__U183(x1) weight: 0 a__U41(x1,x2,x3) weight: (/ 1 16) + x1 + x3 U232(x1) weight: (/ 1 4) + x1 #a__U262(x1) weight: 0 #a__U122(x1) weight: 0 #a__U12(x1,x2,x3) weight: 0 U205(x1,x2) weight: (/ 3 8) a__U205(x1,x2) weight: (/ 3 8) U201(x1,x2,x3) weight: (/ 3 8) U104(x1,x2,x3) weight: (/ 1 4) + x1 + x2 + x3 a__U122(x1) weight: (/ 3 16) a__U14(x1,x2,x3) weight: 0 #a__U81(x1,x2) weight: (/ 1 8) #a__U21(x1,x2,x3) weight: 0 a__U161(x1) weight: (/ 1 8) #a__U61(x1,x2) weight: (/ 5 8) #a__U333(x1,x2) weight: 0 a__U34(x1,x2) weight: 0 U252(x1,x2,x3) weight: (/ 3 16) #a__U261(x1,x2) weight: (/ 1 8) U141(x1) weight: (/ 3 16) + x1 a__fst(x1) weight: 0 tail(x1) weight: (/ 3 16) + x1 a__natsFrom(x1) weight: 0 #a__U302(x1,x2) weight: 0 U83(x1) weight: (/ 5 16) + x1 #a__U294(x1,x2,x3) weight: 0 #mark(x1) weight: 0 a__U204(x1,x2,x3) weight: (/ 3 8) 0() weight: 0 #a__U211(x1) weight: 0 U294(x1,x2,x3) weight: 0 #a__U244(x1,x2,x3) weight: (/ 1 8) a__isLNat(x1) weight: (/ 1 16) U191(x1,x2) weight: (/ 1 8) U343(x1,x2,x3) weight: 0 a__U251(x1,x2,x3) weight: (/ 1 8) U73(x1) weight: (/ 3 16) + x1 #a__U282(x1,x2) weight: 0 a__U21(x1,x2,x3) weight: 0 U332(x1,x2) weight: 0 a__U311(x1,x2) weight: 0 U171(x1,x2) weight: (/ 3 16) + x2 a__U32(x1,x2,x3) weight: 0 a__U91(x1,x2) weight: (/ 1 8) #a__U231(x1,x2) weight: (/ 1 8) sel(x1,x2) weight: (/ 5 16) + x1 + x2 U202(x1,x2,x3) weight: (/ 3 8) afterNth(x1,x2) weight: (/ 1 2) + x1 + x2 #a__U151(x1) weight: 0 #a__U111(x1,x2) weight: (/ 1 8) #a__U161(x1) weight: 0 a__U242(x1,x2,x3) weight: (/ 3 16) + x1 #a__U141(x1) weight: 0 nil() weight: 0 a__splitAt(x1,x2) weight: 0 isLNat(x1) weight: (/ 1 8) + x1 U246(x1) weight: (/ 7 16) + x1 #a__U245(x1,x2) weight: (/ 1 16) U62(x1,x2) weight: (/ 3 16) #a__U52(x1,x2,x3) weight: (/ 3 8) a__U211(x1) weight: (/ 1 8) #a__U102(x1,x2,x3) weight: (/ 1 4) U304(x1,x2) weight: 0 U45(x1,x2) weight: (/ 5 16) + x1 + x2 #a__sel(x1,x2) weight: 0 mark(x1) weight: 0 U151(x1) weight: (/ 3 16) + x1 #a__isLNat(x1) weight: 0 a__U56(x1) weight: (/ 3 16) + x1 #a__U342(x1,x2,x3) weight: 0 a__U72(x1,x2) weight: (/ 1 16) + x1 U334(x1,x2) weight: 0 #a__U101(x1,x2,x3) weight: (/ 5 16) a__U11(x1,x2,x3) weight: 0 U32(x1,x2,x3) weight: 0 a__U53(x1,x2,x3) weight: (/ 1 16) + x1 + x2 + x3 a__U141(x1) weight: (/ 1 8) a__U322(x1,x2,x3,x4) weight: 0 a__sel(x1,x2) weight: 0 a__U42(x1,x2,x3) weight: (/ 1 16) + x1 a__U93(x1) weight: (/ 1 4) U33(x1,x2,x3) weight: 0 #a__U45(x1,x2) weight: (/ 1 16) a__U52(x1,x2,x3) weight: (/ 1 16) + x1 a__U181(x1,x2) weight: (/ 1 8) isLNatKind(x1) weight: (/ 1 8) U14(x1,x2,x3) weight: 0 U211(x1) weight: (/ 3 16) + x1 #a__U243(x1,x2,x3) weight: (/ 3 16) #a__U54(x1,x2,x3) weight: (/ 1 4) U203(x1,x2,x3) weight: (/ 3 8) #a__U105(x1,x2) weight: (/ 1 16) #a__U202(x1,x2,x3) weight: (/ 3 16) + x2 a__U12(x1,x2,x3) weight: 0 U327(x1,x2) weight: 0 #a__U104(x1,x2,x3) weight: (/ 1 8) #a__U201(x1,x2,x3) weight: (/ 1 4) + x2 #a__U63(x1) weight: 0 a__isPLNat(x1) weight: (/ 1 16) + x1 a__U327(x1,x2) weight: 0 U46(x1) weight: (/ 3 8) + x1 #a__U332(x1,x2) weight: 0 a__U326(x1,x2,x3,x4) weight: 0 U251(x1,x2,x3) weight: (/ 3 16) #a__U322(x1,x2,x3,x4) weight: 0 a__isLNatKind(x1) weight: (/ 1 16) #a__U121(x1,x2) weight: (/ 1 8) U52(x1,x2,x3) weight: (/ 1 8) + x2 + x3 #a__U254(x1,x2,x3) weight: (/ 1 4) #a__U324(x1,x2,x3,x4) weight: 0 #a__U281(x1,x2) weight: 0 #a__U251(x1,x2,x3) weight: (/ 7 16) U61(x1,x2) weight: (/ 3 16) + x1 + x2 a__U46(x1) weight: (/ 5 16) #a__U22(x1,x2,x3) weight: 0 a__U13(x1,x2,x3) weight: 0 a__U304(x1,x2) weight: 0 U31(x1,x2,x3) weight: 0 #a__U83(x1) weight: 0 #a__U171(x1,x2) weight: (/ 1 8) a__U71(x1,x2) weight: (/ 1 16) + x1 U183(x1) weight: 0 U245(x1,x2) weight: (/ 3 8) + x1 + x2 U92(x1,x2) weight: (/ 1 4) + x1 + x2 #a__isPLNat(x1) weight: (/ 1 2) #a__U203(x1,x2,x3) weight: (/ 1 8) + x2 head(x1) weight: (/ 1 16) + x1 #a__afterNth(x1,x2) weight: 0 U112(x1) weight: (/ 1 4) + x1 #a__U343(x1,x2,x3) weight: 0 #a__splitAt(x1,x2) weight: 0 #a__isPLNatKind(x1) weight: (/ 1 8) #a__U192(x1,x2) weight: (/ 1 16) a__U255(x1,x2) weight: (/ 3 16) + x1 cons(x1,x2) weight: (/ 1 2) + x1 + x2 a__U344(x1,x2,x3) weight: 0 a__U92(x1,x2) weight: (/ 3 16) U323(x1,x2,x3,x4) weight: 0 a__U61(x1,x2) weight: (/ 1 8) U102(x1,x2,x3) weight: (/ 3 16) + x3 a__U105(x1,x2) weight: (/ 1 4) a__U334(x1,x2) weight: 0 snd(x1) weight: (/ 3 16) + x1 a__take(x1,x2) weight: 0 U256(x1) weight: (/ 5 16) + x1 a__U301(x1,x2,x3) weight: 0 U81(x1,x2) weight: (/ 3 16) + x1 + x2 #a__U41(x1,x2,x3) weight: (/ 7 16) U82(x1,x2) weight: (/ 1 4) + x1 + x2 #a__U304(x1,x2) weight: 0 tt() weight: 0 a__isNatural(x1) weight: (/ 1 16) + x1 a__isNaturalKind(x1) weight: (/ 1 16) a__U131(x1) weight: (/ 1 8) #a__isNatural(x1) weight: x1 U13(x1,x2,x3) weight: 0 #a__fst(x1) weight: 0 a__U23(x1,x2,x3) weight: 0 #a__U311(x1,x2) weight: 0 a__U201(x1,x2,x3) weight: (/ 3 8) #a__U271(x1,x2) weight: (/ 1 8) a__U202(x1,x2,x3) weight: (/ 3 8) U321(x1,x2,x3,x4) weight: 0 a__U282(x1,x2) weight: 0 #a__U241(x1,x2,x3) weight: (/ 5 16) a__U183(x1) weight: 0 a__U333(x1,x2) weight: 0 U22(x1,x2,x3) weight: 0 #a__U293(x1,x2,x3) weight: 0 U51(x1,x2,x3) weight: (/ 1 8) U311(x1,x2) weight: 0 #a__U325(x1,x2,x3,x4) weight: 0 #a__U34(x1,x2) weight: 0 U322(x1,x2,x3,x4) weight: 0 U344(x1,x2,x3) weight: 0 a__U342(x1,x2,x3) weight: 0 a__tail(x1) weight: 0 a__U103(x1,x2,x3) weight: (/ 1 8) + x1 a__U54(x1,x2,x3) weight: (/ 1 8) a__isPLNatKind(x1) weight: (/ 1 16) U53(x1,x2,x3) weight: (/ 1 8) a__U303(x1,x2) weight: 0 a__U323(x1,x2,x3,x4) weight: 0 #a__U55(x1,x2) weight: (/ 1 16) a__U112(x1) weight: (/ 3 16) #a__U331(x1,x2,x3) weight: 0 U41(x1,x2,x3) weight: (/ 1 8) + x2 #a__tail(x1) weight: 0 a__U203(x1,x2,x3) weight: (/ 3 8) #a__U32(x1,x2,x3) weight: 0 #a__U221(x1) weight: 0 a__U101(x1,x2,x3) weight: (/ 1 16) + x1 + x2 + x3 #a__U91(x1,x2) weight: (/ 1 8) a__U341(x1,x2,x3) weight: 0 U282(x1,x2) weight: 0 a__U256(x1) weight: (/ 1 4) U121(x1,x2) weight: (/ 3 16) + x1 a__head(x1) weight: 0 U181(x1,x2) weight: (/ 1 8) U324(x1,x2,x3,x4) weight: 0 U331(x1,x2,x3) weight: 0 U122(x1) weight: (/ 1 4) + x1 a__U312(x1,x2) weight: 0 #a__U327(x1,x2) weight: 0 Usable rules: { } Removed DPs: #7 #184 #242 #308 #344 Number of SCCs: 1, DPs: 238, edges: 25468 SCC { #3 #9 #10 #12 #14 #15 #17..19 #21 #24 #25 #27 #28 #35 #37 #39 #40 #42 #44 #45 #47 #52 #56..61 #65 #67..70 #72 #79 #80 #83 #85 #86 #88 #90..94 #96 #99 #102 #103 #108 #113..115 #117 #119 #120 #122 #123 #130 #133 #134 #136 #140 #141 #147..150 #153 #156 #157 #161 #163 #164 #166 #167 #169..175 #177 #186 #188..191 #194 #198 #205 #207 #208 #210 #215 #216 #218..221 #227 #228 #230 #232 #236..240 #244 #246 #254 #258 #262 #265 #268 #270 #272 #275..277 #281 #282 #284 #287 #289 #292 #295 #297 #304 #306 #310..313 #318 #319 #321..326 #328 #330 #331 #333..338 #340 #342 #343 #347 #350 #354..357 #359 #361 #362 #365 #369 #371 #373..377 #379..381 #384 #389 #391 #393 #395 #397 #399..402 #405..407 #410 #412 #413 #415 #418..420 #422 #423 #429..432 #440..444 #446..448 #452 #455..457 #462..464 #466..473 #476..478 #482..484 #487 #488 #491 #496..498 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. U291(x1,x2,x3) weight: max{x3, (/ 11 16) + x2, (/ 11 16) + x1} #a__U193(x1) weight: 0 a__U83(x1) weight: x1 U231(x1,x2) weight: max{0, x1} U301(x1,x2,x3) weight: max{x3, x2, x1} a__U293(x1,x2,x3) weight: max{x3, (/ 1 2) + x2, x1} a__U241(x1,x2,x3) weight: max{x3, x2, x1} U204(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, (/ 1 16) + x1} a__U324(x1,x2,x3,x4) weight: max{x4, x3, (/ 1 8) + x2, (/ 1 16) + x1} a__U302(x1,x2) weight: max{x2, x1} #a__isNaturalKind(x1) weight: 0 a__U325(x1,x2,x3,x4) weight: max{x4, x3, (/ 1 8) + x2, x1} a__U151(x1) weight: x1 a__U292(x1,x2,x3) weight: max{x3, (/ 9 16) + x2, (/ 11 16) + x1} #a__U73(x1) weight: 0 #a__U131(x1) weight: 0 a__U63(x1) weight: x1 U21(x1,x2,x3) weight: max{x3, x2, x1} U261(x1,x2) weight: max{0, x1} a__U102(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, x1} U254(x1,x2,x3) weight: max{x3, x2, (/ 1 16) + x1} U333(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 8) + x1} #a__U82(x1,x2) weight: 0 a__U332(x1,x2) weight: max{(/ 3 16) + x2, (/ 3 16) + x1} a__U45(x1,x2) weight: max{x2, (/ 1 16) + x1} U193(x1) weight: x1 #a__U72(x1,x2) weight: 0 #a__U242(x1,x2,x3) weight: 0 a__U246(x1) weight: x1 U161(x1) weight: x1 #a__U321(x1,x2,x3,x4) weight: max{0, (/ 81029 4) + x4, (/ 81029 4) + x3, (/ 162059 8) + x2} #a__U71(x1,x2) weight: 0 a__U232(x1) weight: x1 U182(x1,x2) weight: max{x2, x1} #a__U291(x1,x2,x3) weight: max{(/ 81029 4) + x3, (/ 162063 8) + x2, (/ 324127 16) + x1} U11(x1,x2,x3) weight: max{x3, (/ 3 8) + x2, (/ 3 8) + x1} a__U171(x1,x2) weight: max{0, x1} #a__U92(x1,x2) weight: 0 a__U104(x1,x2,x3) weight: max{x3, x2, (/ 1 16) + x1} a__U294(x1,x2,x3) weight: max{x3, (/ 3 8) + x2, (/ 7 16) + x1} a__U182(x1,x2) weight: max{x2, x1} a__U191(x1,x2) weight: max{x2, x1} a__U281(x1,x2) weight: max{(/ 1 4) + x2, (/ 3 16) + x1} U243(x1,x2,x3) weight: max{x3, x2, x1} a__U245(x1,x2) weight: max{x2, x1} #a__U112(x1) weight: 0 s(x1) weight: x1 U105(x1,x2) weight: max{x2, x1} U303(x1,x2) weight: max{x2, x1} #a__U292(x1,x2,x3) weight: max{(/ 81029 4) + x3, (/ 81031 4) + x2, (/ 162063 8) + x1} a__U24(x1,x2) weight: max{x2, x1} #a__U341(x1,x2,x3) weight: max{(/ 81029 4) + x3, (/ 324121 16) + x2, (/ 324115 16) + x1} #a__U31(x1,x2,x3) weight: max{(/ 324115 16) + x3, (/ 81029 4) + x2, (/ 81029 4) + x1} a__U243(x1,x2,x3) weight: max{x3, x2, x1} #a__U33(x1,x2,x3) weight: max{(/ 162057 8) + x3, (/ 81029 4) + x2, (/ 1 16) + x1} #a__U93(x1) weight: 0 #a__head(x1) weight: (/ 81029 4) + x1 U192(x1,x2) weight: max{x2, x1} #a__U253(x1,x2,x3) weight: 0 U24(x1,x2) weight: max{x2, x1} a__U33(x1,x2,x3) weight: max{x3, x2, x1} U106(x1) weight: x1 #a__U24(x1,x2) weight: max{0, (/ 81029 4) + x2} #a__natsFrom(x1) weight: (/ 324119 16) + x1 isPLNatKind(x1) weight: 0 #a__U252(x1,x2,x3) weight: 0 #a__U256(x1) weight: 0 a__U244(x1,x2,x3) weight: max{x3, x2, x1} a__U343(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} U242(x1,x2,x3) weight: max{x3, x2, x1} #a__U303(x1,x2) weight: max{0, (/ 81029 4) + x2} U262(x1) weight: x1 U244(x1,x2,x3) weight: max{x3, x2, x1} U272(x1) weight: x1 U56(x1) weight: x1 #a__U191(x1,x2) weight: 0 #a__U272(x1) weight: 0 #a__U23(x1,x2,x3) weight: max{0, (/ 81029 4) + x2} a__U55(x1,x2) weight: max{x2, x1} isPLNat(x1) weight: x1 #a__snd(x1) weight: (/ 81029 4) + x1 a__U331(x1,x2,x3) weight: max{(/ 1 4) + x3, (/ 1 4) + x2, (/ 3 8) + x1} #a__U312(x1,x2) weight: max{0, (/ 81029 4) + x2} a__afterNth(x1,x2) weight: max{x2, (/ 3 8) + x1} U42(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, (/ 1 16) + x1} U91(x1,x2) weight: max{x2, x1} U221(x1) weight: x1 U293(x1,x2,x3) weight: max{x3, (/ 1 2) + x2, x1} a__U73(x1) weight: x1 #a__U106(x1) weight: 0 U325(x1,x2,x3,x4) weight: max{x4, x3, (/ 1 8) + x2, x1} a__U82(x1,x2) weight: max{x2, x1} #a__U182(x1,x2) weight: 0 take(x1,x2) weight: max{x2, (/ 3 8) + x1} #a__U14(x1,x2,x3) weight: max{0, (/ 81029 4) + x3, (/ 324119 16) + x2} U71(x1,x2) weight: max{x2, x1} a__U62(x1,x2) weight: max{x2, x1} a__U44(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, x1} U131(x1) weight: x1 U206(x1) weight: x1 a__U221(x1) weight: x1 U101(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, x1} #a__U43(x1,x2,x3) weight: 0 #a__U334(x1,x2) weight: max{0, (/ 324117 16) + x2} pair(x1,x2) weight: max{x2, x1} U255(x1,x2) weight: max{x2, x1} #a__U326(x1,x2,x3,x4) weight: max{0, (/ 81029 4) + x4, (/ 81029 4) + x3, (/ 162059 8) + x2} a__U261(x1,x2) weight: max{0, x1} fst(x1) weight: x1 U111(x1,x2) weight: max{0, x1} U43(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, (/ 1 8) + x1} #a__U13(x1,x2,x3) weight: max{0, (/ 81029 4) + x3, (/ 40515 2) + x2} a__U121(x1,x2) weight: max{0, x1} a__U262(x1) weight: x1 #a__U246(x1) weight: 0 #a__U44(x1,x2,x3) weight: 0 #a__U204(x1,x2,x3) weight: 0 U103(x1,x2,x3) weight: max{x3, x2, (/ 1 16) + x1} a__U111(x1,x2) weight: max{0, x1} a__U272(x1) weight: x1 natsFrom(x1) weight: (/ 1 4) + x1 U281(x1,x2) weight: max{(/ 1 4) + x2, (/ 3 16) + x1} #a__U103(x1,x2,x3) weight: 0 #a__U301(x1,x2,x3) weight: max{0, (/ 81029 4) + x3} U44(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, x1} U55(x1,x2) weight: max{x2, x1} #a__U46(x1) weight: 0 a__snd(x1) weight: x1 a__U252(x1,x2,x3) weight: max{x3, x2, (/ 1 16) + x1} U253(x1,x2,x3) weight: max{x3, x2, (/ 1 16) + x1} U312(x1,x2) weight: max{x2, x1} #a__U206(x1) weight: 0 #a__U181(x1,x2) weight: 0 a__U193(x1) weight: x1 a__U271(x1,x2) weight: max{0, x1} #a__U51(x1,x2,x3) weight: 0 U341(x1,x2,x3) weight: max{x3, (/ 5 16) + x2, x1} a__U254(x1,x2,x3) weight: max{x3, x2, (/ 1 16) + x1} U23(x1,x2,x3) weight: max{x3, x2, x1} U292(x1,x2,x3) weight: max{x3, (/ 9 16) + x2, (/ 11 16) + x1} U342(x1,x2,x3) weight: max{x3, (/ 1 4) + x2, (/ 1 8) + x1} a__U172(x1) weight: x1 U63(x1) weight: x1 #a__U56(x1) weight: 0 #a__U344(x1,x2,x3) weight: max{0, (/ 81029 4) + x3, (/ 162059 8) + x2} a__U22(x1,x2,x3) weight: max{x3, x2, x1} U172(x1) weight: x1 U93(x1) weight: x1 splitAt(x1,x2) weight: max{x2, (/ 1 8) + x1} isNaturalKind(x1) weight: 0 U326(x1,x2,x3,x4) weight: max{x4, x3, (/ 1 8) + x2, (/ 1 16) + x1} #a__U323(x1,x2,x3,x4) weight: max{0, (/ 81029 4) + x4, (/ 81029 4) + x3, (/ 162059 8) + x2} a__U106(x1) weight: x1 U72(x1,x2) weight: max{x2, x1} #a__U11(x1,x2,x3) weight: max{0, (/ 81029 4) + x3, (/ 162061 8) + x2} a__U291(x1,x2,x3) weight: max{x3, (/ 11 16) + x2, (/ 11 16) + x1} U241(x1,x2,x3) weight: max{x3, x2, x1} U34(x1,x2) weight: max{x2, x1} a__U192(x1,x2) weight: max{x2, x1} a__U31(x1,x2,x3) weight: max{x3, x2, x1} a__U51(x1,x2,x3) weight: max{x3, x2, x1} a__U253(x1,x2,x3) weight: max{x3, x2, (/ 1 16) + x1} a__U81(x1,x2) weight: max{x2, x1} #a__U53(x1,x2,x3) weight: 0 #a__U205(x1,x2) weight: 0 #a__take(x1,x2) weight: max{(/ 81029 4) + x2, (/ 162061 8) + x1} #a__U172(x1) weight: 0 #a__U255(x1,x2) weight: 0 U12(x1,x2,x3) weight: max{x3, (/ 3 8) + x2, (/ 3 8) + x1} a__U43(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, (/ 1 8) + x1} U271(x1,x2) weight: max{0, x1} a__U231(x1,x2) weight: max{0, x1} #a__U232(x1) weight: 0 #a__isLNatKind(x1) weight: 0 #a__U62(x1,x2) weight: 0 a__U321(x1,x2,x3,x4) weight: max{x4, x3, (/ 1 8) + x2, (/ 1 16) + x1} a__U206(x1) weight: x1 isNatural(x1) weight: x1 U302(x1,x2) weight: max{x2, x1} U54(x1,x2,x3) weight: max{x3, x2, x1} #a__U42(x1,x2,x3) weight: 0 #a__U183(x1) weight: 0 a__U41(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, x1} U232(x1) weight: x1 #a__U262(x1) weight: 0 #a__U122(x1) weight: 0 #a__U12(x1,x2,x3) weight: max{0, (/ 81029 4) + x3, (/ 324121 16) + x2} U205(x1,x2) weight: max{x2, (/ 1 16) + x1} a__U205(x1,x2) weight: max{x2, (/ 1 16) + x1} U201(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, x1} U104(x1,x2,x3) weight: max{x3, x2, (/ 1 16) + x1} a__U122(x1) weight: x1 a__U14(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, (/ 1 4) + x1} #a__U81(x1,x2) weight: 0 #a__U21(x1,x2,x3) weight: max{0, (/ 81029 4) + x2, (/ 81029 4) + x1} a__U161(x1) weight: x1 #a__U61(x1,x2) weight: 0 #a__U333(x1,x2) weight: max{0, (/ 324117 16) + x2} a__U34(x1,x2) weight: max{x2, x1} U252(x1,x2,x3) weight: max{x3, x2, (/ 1 16) + x1} #a__U261(x1,x2) weight: 0 U141(x1) weight: x1 a__fst(x1) weight: x1 tail(x1) weight: (/ 7 16) + x1 a__natsFrom(x1) weight: (/ 1 4) + x1 #a__U302(x1,x2) weight: max{0, (/ 81029 4) + x2} U83(x1) weight: x1 #a__U294(x1,x2,x3) weight: max{(/ 81029 4) + x3, (/ 162061 8) + x2, (/ 81029 4) + x1} #mark(x1) weight: (/ 81029 4) + x1 a__U204(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, (/ 1 16) + x1} 0() weight: 0 #a__U211(x1) weight: 0 U294(x1,x2,x3) weight: max{x3, (/ 3 8) + x2, (/ 7 16) + x1} #a__U244(x1,x2,x3) weight: 0 a__isLNat(x1) weight: x1 U191(x1,x2) weight: max{x2, x1} U343(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} a__U251(x1,x2,x3) weight: max{x3, x2, (/ 1 16) + x1} U73(x1) weight: x1 #a__U282(x1,x2) weight: max{(/ 324117 16) + x2, (/ 324117 16) + x1} a__U21(x1,x2,x3) weight: max{x3, x2, x1} U332(x1,x2) weight: max{(/ 3 16) + x2, (/ 3 16) + x1} a__U311(x1,x2) weight: max{x2, x1} U171(x1,x2) weight: max{0, x1} a__U32(x1,x2,x3) weight: max{x3, x2, x1} a__U91(x1,x2) weight: max{x2, x1} #a__U231(x1,x2) weight: 0 sel(x1,x2) weight: max{x2, (/ 11 16) + x1} U202(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, (/ 1 16) + x1} afterNth(x1,x2) weight: max{x2, (/ 3 8) + x1} #a__U151(x1) weight: 0 #a__U111(x1,x2) weight: 0 #a__U161(x1) weight: 0 a__U242(x1,x2,x3) weight: max{x3, x2, x1} #a__U141(x1) weight: 0 nil() weight: 0 a__splitAt(x1,x2) weight: max{x2, (/ 1 8) + x1} isLNat(x1) weight: x1 U246(x1) weight: x1 #a__U245(x1,x2) weight: 0 U62(x1,x2) weight: max{x2, x1} #a__U52(x1,x2,x3) weight: 0 a__U211(x1) weight: x1 #a__U102(x1,x2,x3) weight: 0 U304(x1,x2) weight: max{x2, x1} U45(x1,x2) weight: max{x2, (/ 1 16) + x1} #a__sel(x1,x2) weight: max{(/ 81029 4) + x2, (/ 324127 16) + x1} mark(x1) weight: x1 U151(x1) weight: x1 #a__isLNat(x1) weight: 0 a__U56(x1) weight: x1 #a__U342(x1,x2,x3) weight: max{(/ 81029 4) + x3, (/ 40515 2) + x2, (/ 324117 16) + x1} a__U72(x1,x2) weight: max{x2, x1} U334(x1,x2) weight: max{(/ 1 8) + x2, (/ 3 16) + x1} #a__U101(x1,x2,x3) weight: 0 a__U11(x1,x2,x3) weight: max{x3, (/ 3 8) + x2, (/ 3 8) + x1} U32(x1,x2,x3) weight: max{x3, x2, x1} a__U53(x1,x2,x3) weight: max{x3, x2, x1} a__U141(x1) weight: x1 a__U322(x1,x2,x3,x4) weight: max{x4, x3, (/ 1 8) + x2, x1} a__sel(x1,x2) weight: max{x2, (/ 11 16) + x1} a__U42(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, (/ 1 16) + x1} a__U93(x1) weight: x1 U33(x1,x2,x3) weight: max{x3, x2, x1} #a__U45(x1,x2) weight: 0 a__U52(x1,x2,x3) weight: max{x3, x2, x1} a__U181(x1,x2) weight: max{x2, x1} isLNatKind(x1) weight: 0 U14(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, (/ 1 4) + x1} U211(x1) weight: x1 #a__U243(x1,x2,x3) weight: 0 #a__U54(x1,x2,x3) weight: 0 U203(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, (/ 1 16) + x1} #a__U105(x1,x2) weight: 0 #a__U202(x1,x2,x3) weight: 0 a__U12(x1,x2,x3) weight: max{x3, (/ 3 8) + x2, (/ 3 8) + x1} U327(x1,x2) weight: max{x2, x1} #a__U104(x1,x2,x3) weight: 0 #a__U201(x1,x2,x3) weight: 0 #a__U63(x1) weight: 0 a__isPLNat(x1) weight: x1 a__U327(x1,x2) weight: max{x2, x1} U46(x1) weight: x1 #a__U332(x1,x2) weight: max{0, (/ 162059 8) + x2} a__U326(x1,x2,x3,x4) weight: max{x4, x3, (/ 1 8) + x2, (/ 1 16) + x1} U251(x1,x2,x3) weight: max{x3, x2, (/ 1 16) + x1} #a__U322(x1,x2,x3,x4) weight: max{0, (/ 81029 4) + x4, (/ 81029 4) + x3, (/ 162059 8) + x2} a__isLNatKind(x1) weight: 0 #a__U121(x1,x2) weight: 0 U52(x1,x2,x3) weight: max{x3, x2, x1} #a__U254(x1,x2,x3) weight: 0 #a__U324(x1,x2,x3,x4) weight: max{0, (/ 81029 4) + x4, (/ 81029 4) + x3, (/ 162059 8) + x2} #a__U281(x1,x2) weight: max{0, (/ 162059 8) + x2} #a__U251(x1,x2,x3) weight: 0 U61(x1,x2) weight: max{x2, x1} a__U46(x1) weight: x1 #a__U22(x1,x2,x3) weight: max{0, (/ 81029 4) + x2} a__U13(x1,x2,x3) weight: max{x3, (/ 1 4) + x2, x1} a__U304(x1,x2) weight: max{x2, x1} U31(x1,x2,x3) weight: max{x3, x2, x1} #a__U83(x1) weight: 0 #a__U171(x1,x2) weight: 0 a__U71(x1,x2) weight: max{x2, x1} U183(x1) weight: x1 U245(x1,x2) weight: max{x2, x1} U92(x1,x2) weight: max{x2, x1} #a__isPLNat(x1) weight: 0 #a__U203(x1,x2,x3) weight: 0 head(x1) weight: x1 #a__afterNth(x1,x2) weight: max{(/ 81029 4) + x2, (/ 162061 8) + x1} U112(x1) weight: x1 #a__U343(x1,x2,x3) weight: max{0, (/ 81029 4) + x3, (/ 324119 16) + x2} #a__splitAt(x1,x2) weight: max{(/ 81029 4) + x2, (/ 162059 8) + x1} #a__isPLNatKind(x1) weight: 0 #a__U192(x1,x2) weight: 0 a__U255(x1,x2) weight: max{x2, x1} cons(x1,x2) weight: max{x2, x1} a__U344(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, (/ 1 16) + x1} a__U92(x1,x2) weight: max{x2, x1} U323(x1,x2,x3,x4) weight: max{x4, x3, (/ 1 8) + x2, x1} a__U61(x1,x2) weight: max{x2, x1} U102(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, x1} a__U105(x1,x2) weight: max{x2, x1} a__U334(x1,x2) weight: max{(/ 1 8) + x2, (/ 3 16) + x1} snd(x1) weight: x1 a__take(x1,x2) weight: max{x2, (/ 3 8) + x1} U256(x1) weight: x1 a__U301(x1,x2,x3) weight: max{x3, x2, x1} U81(x1,x2) weight: max{x2, x1} #a__U41(x1,x2,x3) weight: 0 U82(x1,x2) weight: max{x2, x1} #a__U304(x1,x2) weight: max{0, (/ 81029 4) + x2} tt() weight: 0 a__isNatural(x1) weight: x1 a__isNaturalKind(x1) weight: 0 a__U131(x1) weight: x1 #a__isNatural(x1) weight: 0 U13(x1,x2,x3) weight: max{x3, (/ 1 4) + x2, x1} #a__fst(x1) weight: (/ 81029 4) + x1 a__U23(x1,x2,x3) weight: max{x3, x2, x1} #a__U311(x1,x2) weight: max{0, (/ 81029 4) + x2} a__U201(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, x1} #a__U271(x1,x2) weight: 0 a__U202(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, (/ 1 16) + x1} U321(x1,x2,x3,x4) weight: max{x4, x3, (/ 1 8) + x2, (/ 1 16) + x1} a__U282(x1,x2) weight: max{(/ 1 4) + x2, (/ 3 16) + x1} #a__U241(x1,x2,x3) weight: 0 a__U183(x1) weight: x1 a__U333(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 8) + x1} U22(x1,x2,x3) weight: max{x3, x2, x1} #a__U293(x1,x2,x3) weight: max{(/ 81029 4) + x3, (/ 324123 16) + x2, (/ 324115 16) + x1} U51(x1,x2,x3) weight: max{x3, x2, x1} U311(x1,x2) weight: max{x2, x1} #a__U325(x1,x2,x3,x4) weight: max{(/ 81029 4) + x4, (/ 81029 4) + x3, (/ 162059 8) + x2, (/ 81029 4) + x1} #a__U34(x1,x2) weight: max{(/ 81029 4) + x2, (/ 1 16) + x1} U322(x1,x2,x3,x4) weight: max{x4, x3, (/ 1 8) + x2, x1} U344(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, (/ 1 16) + x1} a__U342(x1,x2,x3) weight: max{x3, (/ 1 4) + x2, (/ 1 8) + x1} a__tail(x1) weight: (/ 7 16) + x1 a__U103(x1,x2,x3) weight: max{x3, x2, (/ 1 16) + x1} a__U54(x1,x2,x3) weight: max{x3, x2, x1} a__isPLNatKind(x1) weight: 0 U53(x1,x2,x3) weight: max{x3, x2, x1} a__U303(x1,x2) weight: max{x2, x1} a__U323(x1,x2,x3,x4) weight: max{x4, x3, (/ 1 8) + x2, x1} #a__U55(x1,x2) weight: 0 a__U112(x1) weight: x1 #a__U331(x1,x2,x3) weight: max{(/ 324119 16) + x3, (/ 324119 16) + x2, (/ 324121 16) + x1} U41(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, x1} #a__tail(x1) weight: (/ 162061 8) + x1 a__U203(x1,x2,x3) weight: max{x3, (/ 1 8) + x2, (/ 1 16) + x1} #a__U32(x1,x2,x3) weight: max{(/ 324115 16) + x3, (/ 81029 4) + x2, (/ 81029 4) + x1} #a__U221(x1) weight: 0 a__U101(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, x1} #a__U91(x1,x2) weight: 0 a__U341(x1,x2,x3) weight: max{x3, (/ 5 16) + x2, x1} U282(x1,x2) weight: max{(/ 1 4) + x2, (/ 3 16) + x1} a__U256(x1) weight: x1 U121(x1,x2) weight: max{0, x1} a__head(x1) weight: x1 U181(x1,x2) weight: max{x2, x1} U324(x1,x2,x3,x4) weight: max{x4, x3, (/ 1 8) + x2, (/ 1 16) + x1} U331(x1,x2,x3) weight: max{(/ 1 4) + x3, (/ 1 4) + x2, (/ 3 8) + x1} U122(x1) weight: x1 a__U312(x1,x2) weight: max{x2, x1} #a__U327(x1,x2) weight: max{(/ 81029 4) + x2, (/ 81029 4) + x1} Usable rules: { 1..407 } Removed DPs: #9 #10 #35 #45 #57 #60 #61 #91 #93 #113 #140 #148 #153 #156 #157 #164 #167 #172 #175 #188 #189 #205 #221 #227 #236 #239 #270 #282 #297 #306 #313 #321..323 #325 #330 #335 #337 #338 #343 #355 #384 #397 #418 #419 #444 #446 #448 #452 #457 #463 #471 #491 #497 #498 Number of SCCs: 2, DPs: 182, edges: 13566 SCC { #3 #12 #14 #15 #17..19 #21 #24 #25 #27 #28 #37 #39 #40 #42 #44 #47 #52 #56 #58 #59 #65 #67..70 #72 #79 #80 #83 #85 #86 #88 #90 #92 #94 #96 #99 #102 #103 #108 #114 #115 #117 #119 #120 #122 #123 #130 #133 #134 #136 #141 #147 #149 #150 #161 #163 #166 #169..171 #173 #174 #177 #186 #190 #191 #198 #207 #208 #210 #215 #216 #218..220 #228 #230 #232 #237 #238 #240 #244 #246 #254 #258 #262 #265 #268 #272 #275..277 #281 #284 #287 #289 #292 #295 #304 #310..312 #318 #319 #324 #326 #328 #331 #333 #334 #336 #340 #342 #347 #350 #354 #356 #357 #359 #361 #362 #365 #369 #371 #373..377 #379..381 #389 #391 #393 #395 #399..402 #405..407 #410 #412 #413 #415 #420 #422 #423 #429..432 #440..443 #447 #455 #456 #462 #464 #466..470 #472 #473 #476..478 #482..484 #487 #488 #496 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. U291(x1,x2,x3) weight: max{(/ 177321 8) + x3, (/ 354641 16) + x2, x1} #a__U193(x1) weight: 0 a__U83(x1) weight: x1 U231(x1,x2) weight: max{(/ 88661 4) + x2, (/ 354643 16) + x1} U301(x1,x2,x3) weight: max{x3, x2, x1} a__U293(x1,x2,x3) weight: max{(/ 177319 8) + x3, (/ 354639 16) + x2, (/ 3 16) + x1} a__U241(x1,x2,x3) weight: max{x3, x2, x1} U204(x1,x2,x3) weight: max{0, (/ 1 16) + x3, (/ 1 8) + x1} a__U324(x1,x2,x3,x4) weight: max{x4, (/ 3 16) + x3, (/ 88657 4) + x2, x1} a__U302(x1,x2) weight: max{x2, x1} #a__isNaturalKind(x1) weight: 0 a__U325(x1,x2,x3,x4) weight: max{x4, (/ 3 16) + x3, (/ 88657 4) + x2, x1} a__U151(x1) weight: x1 a__U292(x1,x2,x3) weight: max{(/ 177319 8) + x3, 22165 + x2, (/ 354639 16) + x1} #a__U73(x1) weight: 0 #a__U131(x1) weight: 0 a__U63(x1) weight: x1 U21(x1,x2,x3) weight: max{(/ 3 8) + x3, (/ 1 2) + x2, (/ 3 8) + x1} U261(x1,x2) weight: max{x2, x1} a__U102(x1,x2,x3) weight: max{(/ 354645 16) + x3, (/ 354645 16) + x2, (/ 88661 4) + x1} U254(x1,x2,x3) weight: max{0, x3, (/ 3 16) + x2} U333(x1,x2) weight: max{0, (/ 1 16) + x2} #a__U82(x1,x2) weight: 0 a__U332(x1,x2) weight: max{0, (/ 1 16) + x2} a__U45(x1,x2) weight: max{0, x2} U193(x1) weight: x1 #a__U72(x1,x2) weight: 0 #a__U242(x1,x2,x3) weight: 0 a__U246(x1) weight: x1 U161(x1) weight: (/ 1 16) + x1 #a__U321(x1,x2,x3,x4) weight: max{0, (/ 130377 4) + x4, (/ 521511 16) + x3, (/ 109517 2) + x2} #a__U71(x1,x2) weight: 0 a__U232(x1) weight: (/ 88661 4) + x1 U182(x1,x2) weight: max{x2, x1} #a__U291(x1,x2,x3) weight: max{(/ 438073 8) + x3, (/ 219037 4) + x2, (/ 1 16) + x1} U11(x1,x2,x3) weight: max{x3, (/ 44329 2) + x2, (/ 354633 16) + x1} a__U171(x1,x2) weight: max{(/ 88661 4) + x2, (/ 88661 4) + x1} #a__U92(x1,x2) weight: 0 a__U104(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, (/ 1 4) + x1} a__U294(x1,x2,x3) weight: max{(/ 354637 16) + x3, (/ 354637 16) + x2, (/ 1 4) + x1} a__U182(x1,x2) weight: max{x2, x1} a__U191(x1,x2) weight: max{(/ 1 8) + x2, x1} a__U281(x1,x2) weight: max{(/ 3 16) + x2, x1} U243(x1,x2,x3) weight: max{x3, x2, x1} a__U245(x1,x2) weight: max{x2, x1} #a__U112(x1) weight: 0 s(x1) weight: x1 U105(x1,x2) weight: max{x2, (/ 1 16) + x1} U303(x1,x2) weight: max{x2, x1} #a__U292(x1,x2,x3) weight: max{0, (/ 521511 16) + x3, (/ 876147 16) + x2} a__U24(x1,x2) weight: max{(/ 1 8) + x2, (/ 3 16) + x1} #a__U341(x1,x2,x3) weight: max{0, (/ 438075 8) + x3, (/ 438075 8) + x2} #a__U31(x1,x2,x3) weight: max{0, (/ 260755 8) + x2, (/ 521507 16) + x1} a__U243(x1,x2,x3) weight: max{x3, x2, x1} #a__U33(x1,x2,x3) weight: max{0, (/ 130377 4) + x2} #a__U93(x1) weight: 0 #a__head(x1) weight: (/ 130377 4) + x1 U192(x1,x2) weight: max{(/ 1 8) + x2, x1} #a__U253(x1,x2,x3) weight: 0 U24(x1,x2) weight: max{(/ 1 8) + x2, (/ 3 16) + x1} a__U33(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, x1} U106(x1) weight: x1 #a__U24(x1,x2) weight: max{0, (/ 521509 16) + x2} #a__natsFrom(x1) weight: (/ 324119 16) isPLNatKind(x1) weight: x1 #a__U252(x1,x2,x3) weight: 0 #a__U256(x1) weight: 0 a__U244(x1,x2,x3) weight: max{x3, x2, x1} a__U343(x1,x2,x3) weight: max{(/ 354641 16) + x3, (/ 88661 4) + x2, (/ 354641 16) + x1} U242(x1,x2,x3) weight: max{x3, x2, x1} #a__U303(x1,x2) weight: max{0, (/ 130377 4) + x2} U262(x1) weight: x1 U244(x1,x2,x3) weight: max{x3, x2, x1} U272(x1) weight: x1 U56(x1) weight: x1 #a__U191(x1,x2) weight: 0 #a__U272(x1) weight: 0 #a__U23(x1,x2,x3) weight: max{0, (/ 65189 2) + x2} a__U55(x1,x2) weight: max{x2, (/ 1 16) + x1} isPLNat(x1) weight: x1 #a__snd(x1) weight: (/ 130377 4) + x1 a__U331(x1,x2,x3) weight: max{0, (/ 1 16) + x3, (/ 1 16) + x2} #a__U312(x1,x2) weight: max{0, (/ 130377 4) + x2} a__afterNth(x1,x2) weight: max{x2, (/ 354635 16) + x1} U42(x1,x2,x3) weight: max{0, x3, (/ 1 16) + x1} U91(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 16) + x1} U221(x1) weight: x1 U293(x1,x2,x3) weight: max{(/ 177319 8) + x3, (/ 354639 16) + x2, (/ 3 16) + x1} a__U73(x1) weight: (/ 1 16) + x1 #a__U106(x1) weight: 0 U325(x1,x2,x3,x4) weight: max{x4, (/ 3 16) + x3, (/ 88657 4) + x2, x1} a__U82(x1,x2) weight: max{x2, x1} #a__U182(x1,x2) weight: 0 take(x1,x2) weight: max{(/ 354645 16) + x2, (/ 177323 8) + x1} #a__U14(x1,x2,x3) weight: max{(/ 130377 4) + x3, (/ 109517 2) + x2, (/ 521507 16) + x1} U71(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 16) + x1} a__U62(x1,x2) weight: max{(/ 1 8) + x2, x1} a__U44(x1,x2,x3) weight: max{0, x3, x1} U131(x1) weight: (/ 1 16) + x1 U206(x1) weight: (/ 1 16) + x1 a__U221(x1) weight: x1 U101(x1,x2,x3) weight: max{(/ 354645 16) + x3, (/ 177323 8) + x2, (/ 1 16) + x1} #a__U43(x1,x2,x3) weight: 0 #a__U334(x1,x2) weight: 0 pair(x1,x2) weight: max{x2, x1} U255(x1,x2) weight: max{x2, (/ 1 16) + x1} #a__U326(x1,x2,x3,x4) weight: max{(/ 130377 4) + x4, (/ 130377 4) + x3, (/ 109517 2) + x2, (/ 260753 8) + x1} a__U261(x1,x2) weight: max{x2, x1} fst(x1) weight: (/ 1 2) + x1 U111(x1,x2) weight: max{x2, (/ 1 16) + x1} U43(x1,x2,x3) weight: max{0, x3, x1} #a__U13(x1,x2,x3) weight: max{(/ 130377 4) + x3, (/ 109517 2) + x2, (/ 1 8) + x1} a__U121(x1,x2) weight: max{x2, x1} a__U262(x1) weight: x1 #a__U246(x1) weight: 0 #a__U44(x1,x2,x3) weight: 0 #a__U204(x1,x2,x3) weight: 0 U103(x1,x2,x3) weight: max{(/ 1 4) + x3, (/ 3 16) + x2, (/ 354645 16) + x1} a__U111(x1,x2) weight: max{x2, (/ 1 16) + x1} a__U272(x1) weight: x1 natsFrom(x1) weight: (/ 3 16) + x1 U281(x1,x2) weight: max{(/ 3 16) + x2, x1} #a__U103(x1,x2,x3) weight: 0 #a__U301(x1,x2,x3) weight: max{0, (/ 130377 4) + x3, (/ 521507 16) + x1} U44(x1,x2,x3) weight: max{0, x3, x1} U55(x1,x2) weight: max{x2, (/ 1 16) + x1} #a__U46(x1) weight: 0 a__snd(x1) weight: x1 a__U252(x1,x2,x3) weight: max{0, x3, (/ 3 16) + x2} U253(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} U312(x1,x2) weight: max{x2, x1} #a__U206(x1) weight: 0 #a__U181(x1,x2) weight: 0 a__U193(x1) weight: x1 a__U271(x1,x2) weight: max{x2, (/ 1 16) + x1} #a__U51(x1,x2,x3) weight: 0 U341(x1,x2,x3) weight: max{(/ 88661 4) + x3, (/ 354645 16) + x2, (/ 354643 16) + x1} a__U254(x1,x2,x3) weight: max{0, x3, (/ 3 16) + x2} U23(x1,x2,x3) weight: max{(/ 3 16) + x3, (/ 5 16) + x2, (/ 3 8) + x1} U292(x1,x2,x3) weight: max{(/ 177319 8) + x3, 22165 + x2, (/ 354639 16) + x1} U342(x1,x2,x3) weight: max{(/ 88661 4) + x3, (/ 88661 4) + x2, (/ 354643 16) + x1} a__U172(x1) weight: (/ 1 16) + x1 U63(x1) weight: x1 #a__U56(x1) weight: 0 #a__U344(x1,x2,x3) weight: max{0, (/ 876145 16) + x3, (/ 876147 16) + x2} a__U22(x1,x2,x3) weight: max{(/ 3 8) + x3, (/ 3 8) + x2, x1} U172(x1) weight: (/ 1 16) + x1 U93(x1) weight: (/ 3 16) + x1 splitAt(x1,x2) weight: max{x2, (/ 88657 4) + x1} isNaturalKind(x1) weight: (/ 1 8) + x1 U326(x1,x2,x3,x4) weight: max{x4, (/ 3 16) + x3, (/ 88657 4) + x2, x1} #a__U323(x1,x2,x3,x4) weight: max{0, (/ 130377 4) + x4, (/ 130377 4) + x3, (/ 109517 2) + x2} a__U106(x1) weight: x1 U72(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 16) + x1} #a__U11(x1,x2,x3) weight: max{0, (/ 130377 4) + x3, (/ 876137 16) + x2} a__U291(x1,x2,x3) weight: max{(/ 177321 8) + x3, (/ 354641 16) + x2, x1} U241(x1,x2,x3) weight: max{x3, x2, x1} U34(x1,x2) weight: max{x2, x1} a__U192(x1,x2) weight: max{(/ 1 8) + x2, x1} a__U31(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, (/ 1 16) + x1} a__U51(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} a__U253(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} a__U81(x1,x2) weight: max{x2, x1} #a__U53(x1,x2,x3) weight: 0 #a__U205(x1,x2) weight: 0 #a__take(x1,x2) weight: max{(/ 109519 2) + x2, (/ 876151 16) + x1} #a__U172(x1) weight: 0 #a__U255(x1,x2) weight: 0 U12(x1,x2,x3) weight: max{x3, (/ 354629 16) + x2, (/ 177315 8) + x1} a__U43(x1,x2,x3) weight: max{0, x3, x1} U271(x1,x2) weight: max{x2, (/ 1 16) + x1} a__U231(x1,x2) weight: max{(/ 88661 4) + x2, (/ 354643 16) + x1} #a__U232(x1) weight: 0 #a__isLNatKind(x1) weight: 0 #a__U62(x1,x2) weight: 0 a__U321(x1,x2,x3,x4) weight: max{0, x4, (/ 3 16) + x3, (/ 88657 4) + x2} a__U206(x1) weight: (/ 1 16) + x1 isNatural(x1) weight: (/ 1 8) + x1 U302(x1,x2) weight: max{x2, x1} U54(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} #a__U42(x1,x2,x3) weight: 0 #a__U183(x1) weight: 0 a__U41(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} U232(x1) weight: (/ 88661 4) + x1 #a__U262(x1) weight: 0 #a__U122(x1) weight: 0 #a__U12(x1,x2,x3) weight: max{(/ 130377 4) + x3, (/ 876137 16) + x2, (/ 1 16) + x1} U205(x1,x2) weight: max{0, (/ 1 16) + x2} a__U205(x1,x2) weight: max{0, (/ 1 16) + x2} U201(x1,x2,x3) weight: max{0, (/ 88661 4) + x3, x1} U104(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, (/ 1 4) + x1} a__U122(x1) weight: x1 a__U14(x1,x2,x3) weight: max{x3, (/ 88657 4) + x2, x1} #a__U81(x1,x2) weight: 0 #a__U21(x1,x2,x3) weight: max{0, (/ 260757 8) + x2} a__U161(x1) weight: (/ 1 16) + x1 #a__U61(x1,x2) weight: 0 #a__U333(x1,x2) weight: 0 a__U34(x1,x2) weight: max{x2, x1} U252(x1,x2,x3) weight: max{0, x3, (/ 3 16) + x2} #a__U261(x1,x2) weight: 0 U141(x1) weight: (/ 1 16) + x1 a__fst(x1) weight: (/ 1 2) + x1 tail(x1) weight: (/ 3 16) + x1 a__natsFrom(x1) weight: (/ 3 16) + x1 #a__U302(x1,x2) weight: max{0, (/ 130377 4) + x2} U83(x1) weight: x1 #a__U294(x1,x2,x3) weight: max{(/ 521509 16) + x3, 54759 + x2, (/ 130377 4) + x1} #mark(x1) weight: (/ 130377 4) + x1 a__U204(x1,x2,x3) weight: max{0, (/ 1 16) + x3, (/ 1 8) + x1} 0() weight: (/ 1 16) #a__U211(x1) weight: 0 U294(x1,x2,x3) weight: max{(/ 354637 16) + x3, (/ 354637 16) + x2, (/ 1 4) + x1} #a__U244(x1,x2,x3) weight: 0 a__isLNat(x1) weight: x1 U191(x1,x2) weight: max{(/ 1 8) + x2, x1} U343(x1,x2,x3) weight: max{(/ 354641 16) + x3, (/ 88661 4) + x2, (/ 354641 16) + x1} a__U251(x1,x2,x3) weight: max{0, x3, (/ 3 16) + x2} U73(x1) weight: (/ 1 16) + x1 #a__U282(x1,x2) weight: 0 a__U21(x1,x2,x3) weight: max{(/ 3 8) + x3, (/ 1 2) + x2, (/ 3 8) + x1} U332(x1,x2) weight: max{0, (/ 1 16) + x2} a__U311(x1,x2) weight: max{x2, x1} U171(x1,x2) weight: max{(/ 88661 4) + x2, (/ 88661 4) + x1} a__U32(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, (/ 1 16) + x1} a__U91(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 16) + x1} #a__U231(x1,x2) weight: 0 sel(x1,x2) weight: max{(/ 177321 8) + x2, (/ 354643 16) + x1} U202(x1,x2,x3) weight: max{0, (/ 3 16) + x3} afterNth(x1,x2) weight: max{x2, (/ 354635 16) + x1} #a__U151(x1) weight: 0 #a__U111(x1,x2) weight: 0 #a__U161(x1) weight: 0 a__U242(x1,x2,x3) weight: max{x3, x2, x1} #a__U141(x1) weight: 0 nil() weight: 0 a__splitAt(x1,x2) weight: max{x2, (/ 88657 4) + x1} isLNat(x1) weight: x1 U246(x1) weight: x1 #a__U245(x1,x2) weight: 0 U62(x1,x2) weight: max{(/ 1 8) + x2, x1} #a__U52(x1,x2,x3) weight: 0 a__U211(x1) weight: (/ 1 16) + x1 #a__U102(x1,x2,x3) weight: 0 U304(x1,x2) weight: max{x2, x1} U45(x1,x2) weight: max{0, x2} #a__sel(x1,x2) weight: max{(/ 876149 16) + x2, (/ 876149 16) + x1} mark(x1) weight: x1 U151(x1) weight: x1 #a__isLNat(x1) weight: 0 a__U56(x1) weight: x1 #a__U342(x1,x2,x3) weight: max{0, (/ 876149 16) + x3, (/ 876149 16) + x2} a__U72(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 16) + x1} U334(x1,x2) weight: max{0, (/ 1 16) + x2} #a__U101(x1,x2,x3) weight: 0 a__U11(x1,x2,x3) weight: max{x3, (/ 44329 2) + x2, (/ 354633 16) + x1} U32(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, (/ 1 16) + x1} a__U53(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} a__U141(x1) weight: (/ 1 16) + x1 a__U322(x1,x2,x3,x4) weight: max{x4, (/ 3 16) + x3, (/ 88657 4) + x2, (/ 1 8) + x1} a__sel(x1,x2) weight: max{(/ 177321 8) + x2, (/ 354643 16) + x1} a__U42(x1,x2,x3) weight: max{0, x3, (/ 1 16) + x1} a__U93(x1) weight: (/ 3 16) + x1 U33(x1,x2,x3) weight: max{x3, (/ 1 16) + x2, x1} #a__U45(x1,x2) weight: 0 a__U52(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} a__U181(x1,x2) weight: max{x2, x1} isLNatKind(x1) weight: x1 U14(x1,x2,x3) weight: max{x3, (/ 88657 4) + x2, x1} U211(x1) weight: (/ 1 16) + x1 #a__U243(x1,x2,x3) weight: 0 #a__U54(x1,x2,x3) weight: 0 U203(x1,x2,x3) weight: max{0, (/ 1 8) + x3, (/ 3 16) + x1} #a__U105(x1,x2) weight: 0 #a__U202(x1,x2,x3) weight: 0 a__U12(x1,x2,x3) weight: max{x3, (/ 354629 16) + x2, (/ 177315 8) + x1} U327(x1,x2) weight: max{(/ 3 16) + x2, x1} #a__U104(x1,x2,x3) weight: 0 #a__U201(x1,x2,x3) weight: 0 #a__U63(x1) weight: 0 a__isPLNat(x1) weight: x1 a__U327(x1,x2) weight: max{(/ 3 16) + x2, x1} U46(x1) weight: x1 #a__U332(x1,x2) weight: 0 a__U326(x1,x2,x3,x4) weight: max{x4, (/ 3 16) + x3, (/ 88657 4) + x2, x1} U251(x1,x2,x3) weight: max{0, x3, (/ 3 16) + x2} #a__U322(x1,x2,x3,x4) weight: max{0, (/ 130377 4) + x4, (/ 130377 4) + x3, (/ 109517 2) + x2} a__isLNatKind(x1) weight: x1 #a__U121(x1,x2) weight: 0 U52(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} #a__U254(x1,x2,x3) weight: 0 #a__U324(x1,x2,x3,x4) weight: max{0, (/ 130377 4) + x4, (/ 130377 4) + x3, (/ 109517 2) + x2} #a__U281(x1,x2) weight: 0 #a__U251(x1,x2,x3) weight: 0 U61(x1,x2) weight: max{(/ 1 8) + x2, (/ 1 16) + x1} a__U46(x1) weight: x1 #a__U22(x1,x2,x3) weight: max{0, (/ 521513 16) + x2} a__U13(x1,x2,x3) weight: max{x3, (/ 354629 16) + x2, x1} a__U304(x1,x2) weight: max{x2, x1} U31(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, (/ 1 16) + x1} #a__U83(x1) weight: 0 #a__U171(x1,x2) weight: 0 a__U71(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 16) + x1} U183(x1) weight: x1 U245(x1,x2) weight: max{x2, x1} U92(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 8) + x1} #a__isPLNat(x1) weight: 0 #a__U203(x1,x2,x3) weight: 0 head(x1) weight: x1 #a__afterNth(x1,x2) weight: max{(/ 130377 4) + x2, (/ 876143 16) + x1} U112(x1) weight: x1 #a__U343(x1,x2,x3) weight: max{0, (/ 438073 8) + x3, (/ 219037 4) + x2} #a__splitAt(x1,x2) weight: max{(/ 130377 4) + x2, (/ 109517 2) + x1} #a__isPLNatKind(x1) weight: 0 #a__U192(x1,x2) weight: 0 a__U255(x1,x2) weight: max{x2, (/ 1 16) + x1} cons(x1,x2) weight: max{x2, (/ 3 16) + x1} a__U344(x1,x2,x3) weight: max{(/ 177319 8) + x3, (/ 177321 8) + x2, (/ 88659 4) + x1} a__U92(x1,x2) weight: max{(/ 3 16) + x2, (/ 1 8) + x1} U323(x1,x2,x3,x4) weight: max{x4, (/ 3 16) + x3, (/ 88657 4) + x2, (/ 1 16) + x1} a__U61(x1,x2) weight: max{(/ 1 8) + x2, (/ 1 16) + x1} U102(x1,x2,x3) weight: max{(/ 354645 16) + x3, (/ 354645 16) + x2, (/ 88661 4) + x1} a__U105(x1,x2) weight: max{x2, (/ 1 16) + x1} a__U334(x1,x2) weight: max{0, (/ 1 16) + x2} snd(x1) weight: x1 a__take(x1,x2) weight: max{(/ 354645 16) + x2, (/ 177323 8) + x1} U256(x1) weight: x1 a__U301(x1,x2,x3) weight: max{x3, x2, x1} U81(x1,x2) weight: max{x2, x1} #a__U41(x1,x2,x3) weight: 0 U82(x1,x2) weight: max{x2, x1} #a__U304(x1,x2) weight: max{0, (/ 130377 4) + x2} tt() weight: 0 a__isNatural(x1) weight: (/ 1 8) + x1 a__isNaturalKind(x1) weight: (/ 1 8) + x1 a__U131(x1) weight: (/ 1 16) + x1 #a__isNatural(x1) weight: 0 U13(x1,x2,x3) weight: max{x3, (/ 354629 16) + x2, x1} #a__fst(x1) weight: (/ 521515 16) + x1 a__U23(x1,x2,x3) weight: max{(/ 3 16) + x3, (/ 5 16) + x2, (/ 3 8) + x1} #a__U311(x1,x2) weight: max{(/ 130377 4) + x2, (/ 521507 16) + x1} a__U201(x1,x2,x3) weight: max{0, (/ 88661 4) + x3, x1} #a__U271(x1,x2) weight: 0 a__U202(x1,x2,x3) weight: max{0, (/ 3 16) + x3} U321(x1,x2,x3,x4) weight: max{0, x4, (/ 3 16) + x3, (/ 88657 4) + x2} a__U282(x1,x2) weight: max{(/ 3 16) + x2, x1} #a__U241(x1,x2,x3) weight: 0 a__U183(x1) weight: x1 a__U333(x1,x2) weight: max{0, (/ 1 16) + x2} U22(x1,x2,x3) weight: max{(/ 3 8) + x3, (/ 3 8) + x2, x1} #a__U293(x1,x2,x3) weight: max{0, (/ 260755 8) + x3, (/ 876145 16) + x2} U51(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} U311(x1,x2) weight: max{x2, x1} #a__U325(x1,x2,x3,x4) weight: max{(/ 130377 4) + x4, (/ 130377 4) + x3, (/ 109517 2) + x2, (/ 521507 16) + x1} #a__U34(x1,x2) weight: max{0, (/ 130377 4) + x2} U322(x1,x2,x3,x4) weight: max{x4, (/ 3 16) + x3, (/ 88657 4) + x2, (/ 1 8) + x1} U344(x1,x2,x3) weight: max{(/ 177319 8) + x3, (/ 177321 8) + x2, (/ 88659 4) + x1} a__U342(x1,x2,x3) weight: max{(/ 88661 4) + x3, (/ 88661 4) + x2, (/ 354643 16) + x1} a__tail(x1) weight: (/ 3 16) + x1 a__U103(x1,x2,x3) weight: max{(/ 1 4) + x3, (/ 3 16) + x2, (/ 354645 16) + x1} a__U54(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} a__isPLNatKind(x1) weight: x1 U53(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} a__U303(x1,x2) weight: max{x2, x1} a__U323(x1,x2,x3,x4) weight: max{x4, (/ 3 16) + x3, (/ 88657 4) + x2, (/ 1 16) + x1} #a__U55(x1,x2) weight: 0 a__U112(x1) weight: x1 #a__U331(x1,x2,x3) weight: 0 U41(x1,x2,x3) weight: max{x3, (/ 3 16) + x2, x1} #a__tail(x1) weight: (/ 162061 8) a__U203(x1,x2,x3) weight: max{0, (/ 1 8) + x3, (/ 3 16) + x1} #a__U32(x1,x2,x3) weight: max{0, (/ 130377 4) + x2} #a__U221(x1) weight: 0 a__U101(x1,x2,x3) weight: max{(/ 354645 16) + x3, (/ 177323 8) + x2, (/ 1 16) + x1} #a__U91(x1,x2) weight: 0 a__U341(x1,x2,x3) weight: max{(/ 88661 4) + x3, (/ 354645 16) + x2, (/ 354643 16) + x1} U282(x1,x2) weight: max{(/ 3 16) + x2, x1} a__U256(x1) weight: x1 U121(x1,x2) weight: max{x2, x1} a__head(x1) weight: x1 U181(x1,x2) weight: max{x2, x1} U324(x1,x2,x3,x4) weight: max{x4, (/ 3 16) + x3, (/ 88657 4) + x2, x1} U331(x1,x2,x3) weight: max{0, (/ 1 16) + x3, (/ 1 16) + x2} U122(x1) weight: x1 a__U312(x1,x2) weight: max{x2, x1} #a__U327(x1,x2) weight: max{(/ 130377 4) + x2, (/ 130377 4) + x1} Usable rules: { 1..407 } Removed DPs: #3 #12 #18 #25 #28 #37 #40 #42 #56 #58 #59 #67 #99 #103 #108 #120 #122 #123 #130 #133 #134 #161 #163 #166 #177 #218..220 #228 #230 #232 #237 #238 #240 #262 #284 #289 #295 #312 #324 #326 #328 #331 #333 #334 #336 #340 #342 #350 #356 #357 #359 #361 #362 #371 #374 #375 #389 #391 #406 #407 #410 #423 #429 #430 #440..442 #455 #456 #462 #464 #476 #477 #487 #488 Number of SCCs: 2, DPs: 103, edges: 4766 SCC { #14 #15 #17 #19 #21 #24 #27 #39 #44 #47 #52 #65 #68..70 #72 #79 #80 #83 #85 #86 #88 #90 #92 #94 #96 #102 #114 #115 #117 #119 #136 #141 #147 #149 #150 #169..171 #173 #174 #190 #191 #207 #208 #210 #215 #216 #244 #246 #254 #258 #265 #268 #272 #275..277 #281 #287 #292 #304 #310 #311 #318 #319 #347 #354 #365 #369 #373 #376 #377 #379..381 #393 #395 #399..402 #405 #412 #413 #415 #420 #422 #431 #432 #443 #447 #466..470 #472 #473 #478 #482 #484 #496 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. U291(x1,x2,x3) weight: max{(/ 49 32) + x3, (/ 3 2) + x2, x1} #a__U193(x1) weight: 0 a__U83(x1) weight: (/ 11 16) + x1 U231(x1,x2) weight: 0 U301(x1,x2,x3) weight: max{(/ 9 32) + x3, (/ 11 32) + x2, (/ 13 32) + x1} a__U293(x1,x2,x3) weight: max{0, (/ 47 32) + x3, (/ 3 2) + x2} a__U241(x1,x2,x3) weight: max{(/ 5 32) + x3, (/ 3 16) + x2, (/ 1 2) + x1} U204(x1,x2,x3) weight: max{0, (/ 1 32) + x1} a__U324(x1,x2,x3,x4) weight: max{0, (/ 5 8) + x4, (/ 11 16) + x3, (/ 23 32) + x1} a__U302(x1,x2) weight: max{(/ 1 4) + x2, (/ 11 32) + x1} #a__isNaturalKind(x1) weight: 0 a__U325(x1,x2,x3,x4) weight: max{0, (/ 5 8) + x4, (/ 11 16) + x3, (/ 7 16) + x1} a__U151(x1) weight: x1 a__U292(x1,x2,x3) weight: max{(/ 47 32) + x3, (/ 3 2) + x2, (/ 47 32) + x1} #a__U73(x1) weight: 0 #a__U131(x1) weight: 0 a__U63(x1) weight: (/ 1 16) + x1 U21(x1,x2,x3) weight: max{(/ 1 32) + x3, (/ 17 32) + x2, x1} U261(x1,x2) weight: max{0, x1} a__U102(x1,x2,x3) weight: max{(/ 13 16) + x3, (/ 3 32) + x2, x1} U254(x1,x2,x3) weight: max{0, (/ 1 16) + x3} U333(x1,x2) weight: max{0, (/ 1 32) + x2} #a__U82(x1,x2) weight: 0 a__U332(x1,x2) weight: max{0, (/ 1 32) + x2} a__U45(x1,x2) weight: max{0, (/ 1 16) + x2} U193(x1) weight: x1 #a__U72(x1,x2) weight: 0 #a__U242(x1,x2,x3) weight: 0 a__U246(x1) weight: (/ 1 32) + x1 U161(x1) weight: 0 #a__U321(x1,x2,x3,x4) weight: max{0, (/ 11 16) + x4, (/ 21 32) + x3} #a__U71(x1,x2) weight: 0 a__U232(x1) weight: 0 U182(x1,x2) weight: max{(/ 3 32) + x2, (/ 1 16) + x1} #a__U291(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: max{(/ 11 8) + x3, (/ 25 32) + x2, (/ 13 16) + x1} a__U171(x1,x2) weight: 0 #a__U92(x1,x2) weight: 0 a__U104(x1,x2,x3) weight: max{0, (/ 1 16) + x3} a__U294(x1,x2,x3) weight: max{(/ 47 32) + x3, (/ 47 32) + x2, (/ 23 16) + x1} a__U182(x1,x2) weight: max{(/ 3 32) + x2, (/ 1 16) + x1} a__U191(x1,x2) weight: max{(/ 1 32) + x2, (/ 1 32) + x1} a__U281(x1,x2) weight: max{(/ 1 8) + x2, x1} U243(x1,x2,x3) weight: max{(/ 1 16) + x3, (/ 1 8) + x2, (/ 1 32) + x1} a__U245(x1,x2) weight: max{(/ 1 16) + x2, (/ 3 32) + x1} #a__U112(x1) weight: 0 s(x1) weight: x1 U105(x1,x2) weight: max{0, (/ 1 16) + x2} U303(x1,x2) weight: max{(/ 1 8) + x2, (/ 3 16) + x1} #a__U292(x1,x2,x3) weight: 0 a__U24(x1,x2) weight: max{0, x2} #a__U341(x1,x2,x3) weight: 0 #a__U31(x1,x2,x3) weight: 0 a__U243(x1,x2,x3) weight: max{(/ 1 16) + x3, (/ 1 8) + x2, (/ 1 32) + x1} #a__U33(x1,x2,x3) weight: 0 #a__U93(x1) weight: 0 #a__head(x1) weight: (/ 260753 8) U192(x1,x2) weight: max{(/ 1 32) + x2, (/ 1 32) + x1} #a__U253(x1,x2,x3) weight: 0 U24(x1,x2) weight: max{0, x2} a__U33(x1,x2,x3) weight: max{0, (/ 7 32) + x2, (/ 1 32) + x1} U106(x1) weight: (/ 1 32) + x1 #a__U24(x1,x2) weight: 0 #a__natsFrom(x1) weight: (/ 648231 32) isPLNatKind(x1) weight: 0 #a__U252(x1,x2,x3) weight: 0 #a__U256(x1) weight: 0 a__U244(x1,x2,x3) weight: max{(/ 1 16) + x3, (/ 1 8) + x2, (/ 1 16) + x1} a__U343(x1,x2,x3) weight: max{0, (/ 23 32) + x3, (/ 21 32) + x2} U242(x1,x2,x3) weight: max{(/ 3 32) + x3, (/ 1 8) + x2, (/ 5 32) + x1} #a__U303(x1,x2) weight: max{(/ 1 8) + x2, (/ 7 32) + x1} U262(x1) weight: x1 U244(x1,x2,x3) weight: max{(/ 1 16) + x3, (/ 1 8) + x2, (/ 1 16) + x1} U272(x1) weight: x1 U56(x1) weight: x1 #a__U191(x1,x2) weight: 0 #a__U272(x1) weight: 0 #a__U23(x1,x2,x3) weight: 0 a__U55(x1,x2) weight: max{(/ 1 32) + x2, x1} isPLNat(x1) weight: x1 #a__snd(x1) weight: (/ 1 32) + x1 a__U331(x1,x2,x3) weight: max{(/ 1 16) + x3, (/ 1 32) + x2, (/ 1 32) + x1} #a__U312(x1,x2) weight: max{0, (/ 3 32) + x2} a__afterNth(x1,x2) weight: max{(/ 11 8) + x2, (/ 27 32) + x1} U42(x1,x2,x3) weight: max{0, (/ 3 32) + x3, (/ 1 16) + x1} U91(x1,x2) weight: max{0, (/ 1 16) + x2} U221(x1) weight: x1 U293(x1,x2,x3) weight: max{0, (/ 47 32) + x3, (/ 3 2) + x2} a__U73(x1) weight: 0 #a__U106(x1) weight: 0 U325(x1,x2,x3,x4) weight: max{0, (/ 5 8) + x4, (/ 11 16) + x3, (/ 7 16) + x1} a__U82(x1,x2) weight: max{(/ 11 16) + x2, (/ 23 32) + x1} #a__U182(x1,x2) weight: 0 take(x1,x2) weight: max{(/ 25 32) + x2, (/ 3 4) + x1} #a__U14(x1,x2,x3) weight: max{0, (/ 11 16) + x3} U71(x1,x2) weight: 0 a__U62(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 32) + x1} a__U44(x1,x2,x3) weight: max{0, (/ 1 16) + x3, (/ 1 32) + x1} U131(x1) weight: 0 U206(x1) weight: 0 a__U221(x1) weight: x1 U101(x1,x2,x3) weight: max{0, (/ 13 16) + x3, (/ 25 32) + x2} #a__U43(x1,x2,x3) weight: 0 #a__U334(x1,x2) weight: 0 pair(x1,x2) weight: max{(/ 1 2) + x2, (/ 15 32) + x1} U255(x1,x2) weight: max{0, (/ 1 16) + x2} #a__U326(x1,x2,x3,x4) weight: max{0, (/ 11 16) + x4, (/ 1 8) + x3} a__U261(x1,x2) weight: max{0, x1} fst(x1) weight: (/ 1 16) + x1 U111(x1,x2) weight: 0 U43(x1,x2,x3) weight: max{0, (/ 1 16) + x3} #a__U13(x1,x2,x3) weight: max{0, (/ 23 32) + x3} a__U121(x1,x2) weight: max{0, x1} a__U262(x1) weight: x1 #a__U246(x1) weight: 0 #a__U44(x1,x2,x3) weight: 0 #a__U204(x1,x2,x3) weight: 0 U103(x1,x2,x3) weight: max{(/ 3 32) + x3, (/ 1 16) + x2, (/ 1 8) + x1} a__U111(x1,x2) weight: 0 a__U272(x1) weight: x1 natsFrom(x1) weight: (/ 1 8) + x1 U281(x1,x2) weight: max{(/ 1 8) + x2, x1} #a__U103(x1,x2,x3) weight: 0 #a__U301(x1,x2,x3) weight: max{(/ 5 16) + x3, (/ 3 8) + x2, (/ 7 16) + x1} U44(x1,x2,x3) weight: max{0, (/ 1 16) + x3, (/ 1 32) + x1} U55(x1,x2) weight: max{(/ 1 32) + x2, x1} #a__U46(x1) weight: 0 a__snd(x1) weight: (/ 11 16) + x1 a__U252(x1,x2,x3) weight: max{0, (/ 1 16) + x3, x1} U253(x1,x2,x3) weight: max{0, (/ 1 16) + x3, (/ 1 16) + x1} U312(x1,x2) weight: max{(/ 1 2) + x2, (/ 17 32) + x1} #a__U206(x1) weight: 0 #a__U181(x1,x2) weight: 0 a__U193(x1) weight: x1 a__U271(x1,x2) weight: 0 #a__U51(x1,x2,x3) weight: 0 U341(x1,x2,x3) weight: max{0, (/ 3 4) + x3, (/ 23 32) + x2} a__U254(x1,x2,x3) weight: max{0, (/ 1 16) + x3} U23(x1,x2,x3) weight: max{0, (/ 1 32) + x2} U292(x1,x2,x3) weight: max{(/ 47 32) + x3, (/ 3 2) + x2, (/ 47 32) + x1} U342(x1,x2,x3) weight: max{0, (/ 23 32) + x3, (/ 23 32) + x2} a__U172(x1) weight: 0 U63(x1) weight: (/ 1 16) + x1 #a__U56(x1) weight: 0 #a__U344(x1,x2,x3) weight: 0 a__U22(x1,x2,x3) weight: max{(/ 1 32) + x3, (/ 3 32) + x2, (/ 1 16) + x1} U172(x1) weight: 0 U93(x1) weight: (/ 1 32) + x1 splitAt(x1,x2) weight: max{0, (/ 5 8) + x2} isNaturalKind(x1) weight: 0 U326(x1,x2,x3,x4) weight: max{0, (/ 5 8) + x4, (/ 21 32) + x3, (/ 11 16) + x1} #a__U323(x1,x2,x3,x4) weight: max{0, (/ 11 16) + x4, (/ 19 32) + x3} a__U106(x1) weight: (/ 1 32) + x1 U72(x1,x2) weight: 0 #a__U11(x1,x2,x3) weight: max{0, (/ 13 16) + x3} a__U291(x1,x2,x3) weight: max{(/ 49 32) + x3, (/ 3 2) + x2, x1} U241(x1,x2,x3) weight: max{(/ 5 32) + x3, (/ 3 16) + x2, (/ 1 2) + x1} U34(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} a__U192(x1,x2) weight: max{(/ 1 32) + x2, (/ 1 32) + x1} a__U31(x1,x2,x3) weight: max{0, (/ 1 16) + x3, (/ 7 32) + x2} a__U51(x1,x2,x3) weight: max{(/ 1 32) + x3, (/ 1 16) + x2, (/ 3 32) + x1} a__U253(x1,x2,x3) weight: max{0, (/ 1 16) + x3, (/ 1 16) + x1} a__U81(x1,x2) weight: max{(/ 11 16) + x2, (/ 23 32) + x1} #a__U53(x1,x2,x3) weight: 0 #a__U205(x1,x2) weight: 0 #a__take(x1,x2) weight: 0 #a__U172(x1) weight: 0 #a__U255(x1,x2) weight: 0 U12(x1,x2,x3) weight: max{(/ 11 8) + x3, (/ 11 16) + x2, (/ 11 8) + x1} a__U43(x1,x2,x3) weight: max{0, (/ 1 16) + x3} U271(x1,x2) weight: 0 a__U231(x1,x2) weight: 0 #a__U232(x1) weight: 0 #a__isLNatKind(x1) weight: 0 #a__U62(x1,x2) weight: 0 a__U321(x1,x2,x3,x4) weight: max{0, (/ 5 8) + x4, (/ 3 4) + x3} a__U206(x1) weight: 0 isNatural(x1) weight: (/ 1 32) + x1 U302(x1,x2) weight: max{(/ 1 4) + x2, (/ 11 32) + x1} U54(x1,x2,x3) weight: max{(/ 1 32) + x3, (/ 1 32) + x2, (/ 1 16) + x1} #a__U42(x1,x2,x3) weight: 0 #a__U183(x1) weight: 0 a__U41(x1,x2,x3) weight: max{0, (/ 29 32) + x3, (/ 3 32) + x1} U232(x1) weight: 0 #a__U262(x1) weight: 0 #a__U122(x1) weight: 0 #a__U12(x1,x2,x3) weight: max{0, (/ 25 32) + x3} U205(x1,x2) weight: 0 a__U205(x1,x2) weight: 0 U201(x1,x2,x3) weight: max{0, (/ 1 16) + x2, (/ 1 32) + x1} U104(x1,x2,x3) weight: max{0, (/ 1 16) + x3} a__U122(x1) weight: x1 a__U14(x1,x2,x3) weight: max{(/ 21 16) + x3, (/ 21 32) + x2, (/ 43 32) + x1} #a__U81(x1,x2) weight: 0 #a__U21(x1,x2,x3) weight: 0 a__U161(x1) weight: 0 #a__U61(x1,x2) weight: 0 #a__U333(x1,x2) weight: 0 a__U34(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 8) + x1} U252(x1,x2,x3) weight: max{0, (/ 1 16) + x3, x1} #a__U261(x1,x2) weight: 0 U141(x1) weight: x1 a__fst(x1) weight: (/ 1 16) + x1 tail(x1) weight: (/ 1 16) + x1 a__natsFrom(x1) weight: (/ 1 8) + x1 #a__U302(x1,x2) weight: max{(/ 9 32) + x2, (/ 7 32) + x1} U83(x1) weight: (/ 11 16) + x1 #a__U294(x1,x2,x3) weight: 0 #mark(x1) weight: (/ 1 16) + x1 a__U204(x1,x2,x3) weight: max{0, (/ 1 32) + x1} 0() weight: (/ 1 32) #a__U211(x1) weight: 0 U294(x1,x2,x3) weight: max{(/ 47 32) + x3, (/ 47 32) + x2, (/ 23 16) + x1} #a__U244(x1,x2,x3) weight: 0 a__isLNat(x1) weight: (/ 1 32) + x1 U191(x1,x2) weight: max{(/ 1 32) + x2, (/ 1 32) + x1} U343(x1,x2,x3) weight: max{0, (/ 23 32) + x3, (/ 21 32) + x2} a__U251(x1,x2,x3) weight: max{0, (/ 1 16) + x3} U73(x1) weight: 0 #a__U282(x1,x2) weight: 0 a__U21(x1,x2,x3) weight: max{(/ 1 32) + x3, (/ 17 32) + x2, x1} U332(x1,x2) weight: max{0, (/ 1 32) + x2} a__U311(x1,x2) weight: max{(/ 17 32) + x2, (/ 19 32) + x1} U171(x1,x2) weight: 0 a__U32(x1,x2,x3) weight: max{(/ 1 16) + x3, (/ 7 32) + x2, (/ 1 32) + x1} a__U91(x1,x2) weight: max{0, (/ 1 16) + x2} #a__U231(x1,x2) weight: 0 sel(x1,x2) weight: max{(/ 49 32) + x2, (/ 49 32) + x1} U202(x1,x2,x3) weight: max{0, (/ 1 16) + x1} afterNth(x1,x2) weight: max{(/ 11 8) + x2, (/ 27 32) + x1} #a__U151(x1) weight: 0 #a__U111(x1,x2) weight: 0 #a__U161(x1) weight: 0 a__U242(x1,x2,x3) weight: max{(/ 3 32) + x3, (/ 1 8) + x2, (/ 5 32) + x1} #a__U141(x1) weight: 0 nil() weight: 0 a__splitAt(x1,x2) weight: max{0, (/ 5 8) + x2} isLNat(x1) weight: (/ 1 32) + x1 U246(x1) weight: (/ 1 32) + x1 #a__U245(x1,x2) weight: 0 U62(x1,x2) weight: max{(/ 1 16) + x2, (/ 1 32) + x1} #a__U52(x1,x2,x3) weight: 0 a__U211(x1) weight: 0 #a__U102(x1,x2,x3) weight: 0 U304(x1,x2) weight: max{(/ 1 8) + x2, (/ 1 8) + x1} U45(x1,x2) weight: max{0, (/ 1 16) + x2} #a__sel(x1,x2) weight: 0 mark(x1) weight: x1 U151(x1) weight: x1 #a__isLNat(x1) weight: 0 a__U56(x1) weight: x1 #a__U342(x1,x2,x3) weight: 0 a__U72(x1,x2) weight: 0 U334(x1,x2) weight: max{0, (/ 1 32) + x2} #a__U101(x1,x2,x3) weight: 0 a__U11(x1,x2,x3) weight: max{(/ 11 8) + x3, (/ 25 32) + x2, (/ 13 16) + x1} U32(x1,x2,x3) weight: max{(/ 1 16) + x3, (/ 7 32) + x2, (/ 1 32) + x1} a__U53(x1,x2,x3) weight: max{(/ 1 32) + x3, (/ 1 16) + x2, (/ 3 32) + x1} a__U141(x1) weight: x1 a__U322(x1,x2,x3,x4) weight: max{0, (/ 5 8) + x4, (/ 3 4) + x3, (/ 23 32) + x1} a__sel(x1,x2) weight: max{(/ 49 32) + x2, (/ 49 32) + x1} a__U42(x1,x2,x3) weight: max{0, (/ 3 32) + x3, (/ 1 16) + x1} a__U93(x1) weight: (/ 1 32) + x1 U33(x1,x2,x3) weight: max{0, (/ 7 32) + x2, (/ 1 32) + x1} #a__U45(x1,x2) weight: 0 a__U52(x1,x2,x3) weight: max{(/ 1 32) + x3, (/ 1 16) + x2, (/ 3 32) + x1} a__U181(x1,x2) weight: max{(/ 3 32) + x2, (/ 1 8) + x1} isLNatKind(x1) weight: 0 U14(x1,x2,x3) weight: max{(/ 21 16) + x3, (/ 21 32) + x2, (/ 43 32) + x1} U211(x1) weight: 0 #a__U243(x1,x2,x3) weight: 0 #a__U54(x1,x2,x3) weight: 0 U203(x1,x2,x3) weight: max{0, (/ 1 32) + x1} #a__U105(x1,x2) weight: 0 #a__U202(x1,x2,x3) weight: 0 a__U12(x1,x2,x3) weight: max{(/ 11 8) + x3, (/ 11 16) + x2, (/ 11 8) + x1} U327(x1,x2) weight: max{(/ 19 32) + x2, x1} #a__U104(x1,x2,x3) weight: 0 #a__U201(x1,x2,x3) weight: 0 #a__U63(x1) weight: 0 a__isPLNat(x1) weight: x1 a__U327(x1,x2) weight: max{(/ 19 32) + x2, x1} U46(x1) weight: (/ 1 32) + x1 #a__U332(x1,x2) weight: 0 a__U326(x1,x2,x3,x4) weight: max{0, (/ 5 8) + x4, (/ 21 32) + x3, (/ 11 16) + x1} U251(x1,x2,x3) weight: max{0, (/ 1 16) + x3} #a__U322(x1,x2,x3,x4) weight: max{0, (/ 11 16) + x4, (/ 5 8) + x3} a__isLNatKind(x1) weight: 0 #a__U121(x1,x2) weight: 0 U52(x1,x2,x3) weight: max{(/ 1 32) + x3, (/ 1 16) + x2, (/ 3 32) + x1} #a__U254(x1,x2,x3) weight: 0 #a__U324(x1,x2,x3,x4) weight: max{0, (/ 11 16) + x4, (/ 9 16) + x3} #a__U281(x1,x2) weight: 0 #a__U251(x1,x2,x3) weight: 0 U61(x1,x2) weight: max{0, (/ 1 16) + x2} a__U46(x1) weight: (/ 1 32) + x1 #a__U22(x1,x2,x3) weight: 0 a__U13(x1,x2,x3) weight: max{(/ 43 32) + x3, (/ 11 16) + x2, (/ 43 32) + x1} a__U304(x1,x2) weight: max{(/ 1 8) + x2, (/ 1 8) + x1} U31(x1,x2,x3) weight: max{0, (/ 1 16) + x3, (/ 7 32) + x2} #a__U83(x1) weight: 0 #a__U171(x1,x2) weight: 0 a__U71(x1,x2) weight: 0 U183(x1) weight: (/ 1 32) + x1 U245(x1,x2) weight: max{(/ 1 16) + x2, (/ 3 32) + x1} U92(x1,x2) weight: max{0, (/ 1 16) + x2} #a__isPLNat(x1) weight: 0 #a__U203(x1,x2,x3) weight: 0 head(x1) weight: (/ 3 32) + x1 #a__afterNth(x1,x2) weight: max{0, (/ 15 16) + x2} U112(x1) weight: x1 #a__U343(x1,x2,x3) weight: 0 #a__splitAt(x1,x2) weight: max{0, (/ 11 16) + x2} #a__isPLNatKind(x1) weight: 0 #a__U192(x1,x2) weight: 0 a__U255(x1,x2) weight: max{0, (/ 1 16) + x2} cons(x1,x2) weight: max{x2, (/ 1 8) + x1} a__U344(x1,x2,x3) weight: max{(/ 11 16) + x3, (/ 1 32) + x2, (/ 23 32) + x1} a__U92(x1,x2) weight: max{0, (/ 1 16) + x2} U323(x1,x2,x3,x4) weight: max{0, (/ 5 8) + x4, (/ 23 32) + x3, (/ 11 16) + x1} a__U61(x1,x2) weight: max{0, (/ 1 16) + x2} U102(x1,x2,x3) weight: max{(/ 13 16) + x3, (/ 3 32) + x2, x1} a__U105(x1,x2) weight: max{0, (/ 1 16) + x2} a__U334(x1,x2) weight: max{0, (/ 1 32) + x2} snd(x1) weight: (/ 11 16) + x1 a__take(x1,x2) weight: max{(/ 25 32) + x2, (/ 3 4) + x1} U256(x1) weight: (/ 1 32) + x1 a__U301(x1,x2,x3) weight: max{(/ 9 32) + x3, (/ 11 32) + x2, (/ 13 32) + x1} U81(x1,x2) weight: max{(/ 11 16) + x2, (/ 23 32) + x1} #a__U41(x1,x2,x3) weight: 0 U82(x1,x2) weight: max{(/ 11 16) + x2, (/ 23 32) + x1} #a__U304(x1,x2) weight: max{(/ 3 32) + x2, (/ 5 32) + x1} tt() weight: 0 a__isNatural(x1) weight: (/ 1 32) + x1 a__isNaturalKind(x1) weight: 0 a__U131(x1) weight: 0 #a__isNatural(x1) weight: 0 U13(x1,x2,x3) weight: max{(/ 43 32) + x3, (/ 11 16) + x2, (/ 43 32) + x1} #a__fst(x1) weight: (/ 1043019 32) a__U23(x1,x2,x3) weight: max{0, (/ 1 32) + x2} #a__U311(x1,x2) weight: max{(/ 1 8) + x2, (/ 5 8) + x1} a__U201(x1,x2,x3) weight: max{0, (/ 1 16) + x2, (/ 1 32) + x1} #a__U271(x1,x2) weight: 0 a__U202(x1,x2,x3) weight: max{0, (/ 1 16) + x1} U321(x1,x2,x3,x4) weight: max{0, (/ 5 8) + x4, (/ 3 4) + x3} a__U282(x1,x2) weight: max{(/ 1 8) + x2, (/ 1 8) + x1} #a__U241(x1,x2,x3) weight: 0 a__U183(x1) weight: (/ 1 32) + x1 a__U333(x1,x2) weight: max{0, (/ 1 32) + x2} U22(x1,x2,x3) weight: max{(/ 1 32) + x3, (/ 3 32) + x2, (/ 1 16) + x1} #a__U293(x1,x2,x3) weight: 0 U51(x1,x2,x3) weight: max{(/ 1 32) + x3, (/ 1 16) + x2, (/ 3 32) + x1} U311(x1,x2) weight: max{(/ 17 32) + x2, (/ 19 32) + x1} #a__U325(x1,x2,x3,x4) weight: max{0, (/ 11 16) + x4, (/ 17 32) + x3} #a__U34(x1,x2) weight: max{(/ 3 32) + x2, (/ 5 32) + x1} U322(x1,x2,x3,x4) weight: max{0, (/ 5 8) + x4, (/ 3 4) + x3, (/ 23 32) + x1} U344(x1,x2,x3) weight: max{(/ 11 16) + x3, (/ 1 32) + x2, (/ 23 32) + x1} a__U342(x1,x2,x3) weight: max{0, (/ 23 32) + x3, (/ 23 32) + x2} a__tail(x1) weight: (/ 1 16) + x1 a__U103(x1,x2,x3) weight: max{(/ 3 32) + x3, (/ 1 16) + x2, (/ 1 8) + x1} a__U54(x1,x2,x3) weight: max{(/ 1 32) + x3, (/ 1 32) + x2, (/ 1 16) + x1} a__isPLNatKind(x1) weight: 0 U53(x1,x2,x3) weight: max{(/ 1 32) + x3, (/ 1 16) + x2, (/ 3 32) + x1} a__U303(x1,x2) weight: max{(/ 1 8) + x2, (/ 3 16) + x1} a__U323(x1,x2,x3,x4) weight: max{0, (/ 5 8) + x4, (/ 23 32) + x3, (/ 11 16) + x1} #a__U55(x1,x2) weight: 0 a__U112(x1) weight: x1 #a__U331(x1,x2,x3) weight: 0 U41(x1,x2,x3) weight: max{0, (/ 29 32) + x3, (/ 3 32) + x1} #a__tail(x1) weight: (/ 324117 16) a__U203(x1,x2,x3) weight: max{0, (/ 1 32) + x1} #a__U32(x1,x2,x3) weight: 0 #a__U221(x1) weight: 0 a__U101(x1,x2,x3) weight: max{0, (/ 13 16) + x3, (/ 25 32) + x2} #a__U91(x1,x2) weight: 0 a__U341(x1,x2,x3) weight: max{0, (/ 3 4) + x3, (/ 23 32) + x2} U282(x1,x2) weight: max{(/ 1 8) + x2, (/ 1 8) + x1} a__U256(x1) weight: (/ 1 32) + x1 U121(x1,x2) weight: max{0, x1} a__head(x1) weight: (/ 3 32) + x1 U181(x1,x2) weight: max{(/ 3 32) + x2, (/ 1 8) + x1} U324(x1,x2,x3,x4) weight: max{0, (/ 5 8) + x4, (/ 11 16) + x3, (/ 23 32) + x1} U331(x1,x2,x3) weight: max{(/ 1 16) + x3, (/ 1 32) + x2, (/ 1 32) + x1} U122(x1) weight: x1 a__U312(x1,x2) weight: max{(/ 1 2) + x2, (/ 17 32) + x1} #a__U327(x1,x2) weight: max{(/ 3 32) + x2, (/ 1 16) + x1} Usable rules: { 1..407 } Removed DPs: #14 #15 #17 #19 #21 #27 #39 #65 #69 #79 #83 #85 #86 #92 #96 #102 #114 #115 #117 #136 #141 #147 #149 #150 #169 #173 #174 #207 #208 #215 #216 #244 #246 #258 #265 #268 #272 #275..277 #287 #304 #310 #311 #318 #319 #347 #354 #369 #373 #376 #377 #380 #381 #399..402 #405 #412 #413 #420 #431 #432 #447 #466..469 #472 #473 #478 #484 #496 Number of SCCs: 3, DPs: 19, edges: 151 SCC { #47 #94 #119 #191 #210 #254 #365 #379 #393 #395 #415 #482 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U291(x1,x2,x3) weight: (/ 3 16) + x1 #a__U193(x1) weight: 0 a__U83(x1) weight: (/ 7 16) U231(x1,x2) weight: (/ 1 16) + x1 U301(x1,x2,x3) weight: (/ 7 32) a__U293(x1,x2,x3) weight: (/ 5 32) a__U241(x1,x2,x3) weight: (/ 7 16) + x3 U204(x1,x2,x3) weight: (/ 5 16) + x1 + x2 a__U324(x1,x2,x3,x4) weight: (/ 1 32) + x1 + x2 + x3 + x4 a__U302(x1,x2) weight: (/ 7 32) + x2 #a__isNaturalKind(x1) weight: 0 a__U325(x1,x2,x3,x4) weight: (/ 5 32) + x3 a__U151(x1) weight: (/ 15 32) a__U292(x1,x2,x3) weight: (/ 1 8) + x1 + x3 #a__U73(x1) weight: 0 #a__U131(x1) weight: 0 a__U63(x1) weight: (/ 7 16) U21(x1,x2,x3) weight: (/ 7 32) + x1 U261(x1,x2) weight: (/ 7 32) + x1 + x2 a__U102(x1,x2,x3) weight: (/ 1 8) + x1 + x2 + x3 U254(x1,x2,x3) weight: (/ 1 4) U333(x1,x2) weight: (/ 1 16) #a__U82(x1,x2) weight: (/ 1 32) a__U332(x1,x2) weight: (/ 5 32) + x2 a__U45(x1,x2) weight: (/ 5 32) + x1 + x2 U193(x1) weight: (/ 9 32) + x1 #a__U72(x1,x2) weight: (/ 1 8) #a__U242(x1,x2,x3) weight: (/ 1 8) a__U246(x1) weight: (/ 19 32) U161(x1) weight: (/ 1 2) #a__U321(x1,x2,x3,x4) weight: 0 #a__U71(x1,x2) weight: (/ 5 32) a__U232(x1) weight: (/ 5 32) U182(x1,x2) weight: (/ 1 16) #a__U291(x1,x2,x3) weight: (/ 1 32) U11(x1,x2,x3) weight: (/ 3 16) + x3 a__U171(x1,x2) weight: (/ 3 16) + x1 + x2 #a__U92(x1,x2) weight: (/ 1 32) a__U104(x1,x2,x3) weight: (/ 3 16) + x2 a__U294(x1,x2,x3) weight: (/ 3 16) + x2 + x3 a__U182(x1,x2) weight: (/ 1 32) + x1 + x2 a__U191(x1,x2) weight: (/ 3 16) + x2 a__U281(x1,x2) weight: (/ 3 16) + x2 U243(x1,x2,x3) weight: (/ 17 32) a__U245(x1,x2) weight: (/ 9 16) #a__U112(x1) weight: 0 s(x1) weight: (/ 1 32) + x1 U105(x1,x2) weight: (/ 1 4) + x1 U303(x1,x2) weight: (/ 9 32) + x1 #a__U292(x1,x2,x3) weight: (/ 1 32) a__U24(x1,x2) weight: (/ 3 32) #a__U341(x1,x2,x3) weight: (/ 1 32) #a__U31(x1,x2,x3) weight: (/ 1 32) a__U243(x1,x2,x3) weight: (/ 1 2) + x3 #a__U33(x1,x2,x3) weight: (/ 1 32) #a__U93(x1) weight: 0 #a__head(x1) weight: (/ 1 32) U192(x1,x2) weight: (/ 1 4) + x2 #a__U253(x1,x2,x3) weight: (/ 5 32) U24(x1,x2) weight: (/ 1 8) + x1 + x2 a__U33(x1,x2,x3) weight: (/ 5 16) + x2 + x3 U106(x1) weight: (/ 9 32) + x1 #a__U24(x1,x2) weight: (/ 1 32) #a__natsFrom(x1) weight: 0 isPLNatKind(x1) weight: (/ 3 16) #a__U252(x1,x2,x3) weight: (/ 3 16) #a__U256(x1) weight: 0 a__U244(x1,x2,x3) weight: (/ 17 32) a__U343(x1,x2,x3) weight: (/ 1 16) + x1 + x2 + x3 U242(x1,x2,x3) weight: (/ 1 2) + x2 #a__U303(x1,x2) weight: 0 U262(x1) weight: (/ 1 4) + x1 U244(x1,x2,x3) weight: (/ 9 16) U272(x1) weight: (/ 3 16) + x1 U56(x1) weight: (/ 5 8) + x1 #a__U191(x1,x2) weight: (/ 1 16) #a__U272(x1) weight: 0 #a__U23(x1,x2,x3) weight: (/ 1 32) a__U55(x1,x2) weight: (/ 9 16) + x2 isPLNat(x1) weight: (/ 3 16) #a__snd(x1) weight: 0 a__U331(x1,x2,x3) weight: (/ 1 32) + x1 #a__U312(x1,x2) weight: 0 a__afterNth(x1,x2) weight: (/ 1 32) + x1 U42(x1,x2,x3) weight: (/ 5 32) + x1 U91(x1,x2) weight: (/ 13 32) + x1 U221(x1) weight: (/ 7 32) + x1 U293(x1,x2,x3) weight: (/ 3 16) + x1 a__U73(x1) weight: (/ 7 16) #a__U106(x1) weight: 0 U325(x1,x2,x3,x4) weight: (/ 3 16) + x2 + x4 a__U82(x1,x2) weight: (/ 13 32) + x2 #a__U182(x1,x2) weight: (/ 1 32) take(x1,x2) weight: (/ 1 16) + x2 #a__U14(x1,x2,x3) weight: 0 U71(x1,x2) weight: (/ 13 32) + x1 + x2 a__U62(x1,x2) weight: (/ 13 32) + x2 a__U44(x1,x2,x3) weight: (/ 1 8) + x2 U131(x1) weight: (/ 1 2) + x1 U206(x1) weight: (/ 1 16) a__U221(x1) weight: (/ 3 16) U101(x1,x2,x3) weight: (/ 9 32) + x1 + x2 + x3 #a__U43(x1,x2,x3) weight: (/ 5 32) #a__U334(x1,x2) weight: 0 pair(x1,x2) weight: (/ 1 4) + x1 U255(x1,x2) weight: (/ 1 8) #a__U326(x1,x2,x3,x4) weight: 0 a__U261(x1,x2) weight: (/ 3 16) fst(x1) weight: (/ 3 16) + x1 U111(x1,x2) weight: (/ 3 8) + x2 U43(x1,x2,x3) weight: (/ 3 16) + x1 + x2 #a__U13(x1,x2,x3) weight: 0 a__U121(x1,x2) weight: (/ 17 32) a__U262(x1) weight: (/ 7 32) #a__U246(x1) weight: 0 #a__U44(x1,x2,x3) weight: (/ 1 8) #a__U204(x1,x2,x3) weight: (/ 1 32) U103(x1,x2,x3) weight: (/ 3 16) + x1 + x3 a__U111(x1,x2) weight: (/ 11 32) a__U272(x1) weight: (/ 5 32) natsFrom(x1) weight: (/ 3 16) U281(x1,x2) weight: (/ 7 32) + x1 #a__U103(x1,x2,x3) weight: (/ 3 32) #a__U301(x1,x2,x3) weight: 0 U44(x1,x2,x3) weight: (/ 5 32) U55(x1,x2) weight: (/ 19 32) + x1 #a__U46(x1) weight: 0 a__snd(x1) weight: (/ 5 32) a__U252(x1,x2,x3) weight: (/ 13 32) + x2 U253(x1,x2,x3) weight: (/ 15 32) + x1 + x3 U312(x1,x2) weight: (/ 1 4) #a__U206(x1) weight: 0 #a__U181(x1,x2) weight: (/ 1 16) a__U193(x1) weight: (/ 1 4) a__U271(x1,x2) weight: (/ 1 32) + x1 + x2 #a__U51(x1,x2,x3) weight: (/ 7 32) U341(x1,x2,x3) weight: (/ 3 16) + x1 + x3 a__U254(x1,x2,x3) weight: (/ 7 32) + x1 + x2 + x3 U23(x1,x2,x3) weight: (/ 3 32) + x1 + x3 U292(x1,x2,x3) weight: (/ 5 32) + x2 U342(x1,x2,x3) weight: (/ 7 32) + x1 + x2 a__U172(x1) weight: (/ 7 32) U63(x1) weight: (/ 15 32) + x1 #a__U56(x1) weight: 0 #a__U344(x1,x2,x3) weight: (/ 1 32) a__U22(x1,x2,x3) weight: (/ 1 32) + x1 + x2 U172(x1) weight: (/ 1 4) U93(x1) weight: (/ 5 16) splitAt(x1,x2) weight: (/ 3 16) + x1 isNaturalKind(x1) weight: (/ 3 16) + x1 U326(x1,x2,x3,x4) weight: (/ 1 16) + x1 + x3 + x4 #a__U323(x1,x2,x3,x4) weight: 0 a__U106(x1) weight: (/ 1 4) U72(x1,x2) weight: (/ 7 16) + x1 + x2 #a__U11(x1,x2,x3) weight: 0 a__U291(x1,x2,x3) weight: (/ 5 32) + x2 + x3 U241(x1,x2,x3) weight: (/ 15 32) U34(x1,x2) weight: (/ 3 8) + x2 a__U192(x1,x2) weight: (/ 7 32) a__U31(x1,x2,x3) weight: (/ 1 4) + x3 a__U51(x1,x2,x3) weight: (/ 7 16) + x3 a__U253(x1,x2,x3) weight: (/ 7 16) a__U81(x1,x2) weight: (/ 3 8) + x2 #a__U53(x1,x2,x3) weight: (/ 5 32) #a__U205(x1,x2) weight: (/ 1 32) #a__take(x1,x2) weight: (/ 1 32) #a__U172(x1) weight: 0 #a__U255(x1,x2) weight: (/ 1 32) U12(x1,x2,x3) weight: (/ 7 32) + x1 a__U43(x1,x2,x3) weight: (/ 5 32) U271(x1,x2) weight: (/ 1 16) a__U231(x1,x2) weight: (/ 1 32) + x1 + x2 #a__U232(x1) weight: 0 #a__isLNatKind(x1) weight: (/ 1 32) #a__U62(x1,x2) weight: (/ 9 32) a__U321(x1,x2,x3,x4) weight: (/ 3 16) a__U206(x1) weight: (/ 1 32) + x1 isNatural(x1) weight: (/ 3 16) U302(x1,x2) weight: (/ 1 4) + x1 U54(x1,x2,x3) weight: (/ 9 16) + x1 #a__U42(x1,x2,x3) weight: (/ 3 16) #a__U183(x1) weight: 0 a__U41(x1,x2,x3) weight: (/ 1 4) U232(x1) weight: (/ 3 16) + x1 #a__U262(x1) weight: 0 #a__U122(x1) weight: 0 #a__U12(x1,x2,x3) weight: 0 U205(x1,x2) weight: (/ 3 16) a__U205(x1,x2) weight: (/ 5 32) + x1 + x2 U201(x1,x2,x3) weight: (/ 7 32) + x1 U104(x1,x2,x3) weight: (/ 7 32) + x1 + x3 a__U122(x1) weight: (/ 9 16) a__U14(x1,x2,x3) weight: (/ 1 32) + x1 + x3 #a__U81(x1,x2) weight: (/ 1 16) #a__U21(x1,x2,x3) weight: (/ 1 32) a__U161(x1) weight: (/ 15 32) #a__U61(x1,x2) weight: (/ 5 16) #a__U333(x1,x2) weight: 0 a__U34(x1,x2) weight: (/ 11 32) U252(x1,x2,x3) weight: (/ 7 16) + x1 + x3 #a__U261(x1,x2) weight: (/ 1 16) U141(x1) weight: (/ 1 2) a__fst(x1) weight: (/ 5 32) tail(x1) weight: (/ 3 16) + x1 a__natsFrom(x1) weight: (/ 5 32) #a__U302(x1,x2) weight: 0 U83(x1) weight: (/ 15 32) + x1 #a__U294(x1,x2,x3) weight: (/ 1 32) #mark(x1) weight: x1 a__U204(x1,x2,x3) weight: (/ 9 32) 0() weight: 0 #a__U211(x1) weight: 0 U294(x1,x2,x3) weight: (/ 7 32) + x1 #a__U244(x1,x2,x3) weight: (/ 1 16) a__isLNat(x1) weight: (/ 5 32) + x1 U191(x1,x2) weight: (/ 7 32) + x1 U343(x1,x2,x3) weight: (/ 3 32) a__U251(x1,x2,x3) weight: (/ 3 8) U73(x1) weight: (/ 15 32) #a__U282(x1,x2) weight: 0 a__U21(x1,x2,x3) weight: (/ 3 16) + x2 + x3 U332(x1,x2) weight: (/ 3 16) + x1 a__U311(x1,x2) weight: (/ 3 16) U171(x1,x2) weight: (/ 7 32) a__U32(x1,x2,x3) weight: (/ 9 32) a__U91(x1,x2) weight: (/ 3 8) #a__U231(x1,x2) weight: (/ 1 16) sel(x1,x2) weight: (/ 1 16) + x1 U202(x1,x2,x3) weight: (/ 1 4) + x1 afterNth(x1,x2) weight: (/ 1 16) + x1 + x2 #a__U151(x1) weight: 0 #a__U111(x1,x2) weight: (/ 1 16) #a__U161(x1) weight: 0 a__U242(x1,x2,x3) weight: (/ 15 32) #a__U141(x1) weight: 0 nil() weight: 0 a__splitAt(x1,x2) weight: (/ 5 32) isLNat(x1) weight: (/ 3 16) U246(x1) weight: (/ 5 8) #a__U245(x1,x2) weight: (/ 1 32) U62(x1,x2) weight: (/ 7 16) #a__U52(x1,x2,x3) weight: (/ 3 16) a__U211(x1) weight: (/ 1 32) + x1 #a__U102(x1,x2,x3) weight: (/ 1 8) U304(x1,x2) weight: (/ 1 16) + x2 U45(x1,x2) weight: (/ 3 16) #a__sel(x1,x2) weight: (/ 1 32) mark(x1) weight: (/ 1 8) U151(x1) weight: (/ 1 2) + x1 #a__isLNat(x1) weight: 0 a__U56(x1) weight: (/ 19 32) #a__U342(x1,x2,x3) weight: (/ 1 32) a__U72(x1,x2) weight: (/ 13 32) U334(x1,x2) weight: (/ 1 8) #a__U101(x1,x2,x3) weight: (/ 5 32) a__U11(x1,x2,x3) weight: (/ 5 32) U32(x1,x2,x3) weight: (/ 5 16) + x3 a__U53(x1,x2,x3) weight: (/ 1 2) a__U141(x1) weight: (/ 15 32) a__U322(x1,x2,x3,x4) weight: (/ 1 8) + x1 a__sel(x1,x2) weight: (/ 1 32) + x1 a__U42(x1,x2,x3) weight: (/ 1 8) + x1 + x2 a__U93(x1) weight: (/ 9 32) + x1 U33(x1,x2,x3) weight: (/ 11 32) #a__U45(x1,x2) weight: (/ 1 32) a__U52(x1,x2,x3) weight: (/ 15 32) + x2 a__U181(x1,x2) weight: (/ 3 16) isLNatKind(x1) weight: (/ 9 32) U14(x1,x2,x3) weight: (/ 1 16) + x1 + x2 U211(x1) weight: (/ 1 16) + x1 #a__U243(x1,x2,x3) weight: (/ 3 32) #a__U54(x1,x2,x3) weight: (/ 1 8) U203(x1,x2,x3) weight: (/ 9 32) + x2 + x3 #a__U105(x1,x2) weight: (/ 1 32) #a__U202(x1,x2,x3) weight: (/ 3 32) a__U12(x1,x2,x3) weight: (/ 3 16) + x2 U327(x1,x2) weight: (/ 3 16) + x1 #a__U104(x1,x2,x3) weight: (/ 1 16) #a__U201(x1,x2,x3) weight: (/ 1 8) #a__U63(x1) weight: 0 a__isPLNat(x1) weight: (/ 5 32) + x1 a__U327(x1,x2) weight: (/ 5 32) + x2 U46(x1) weight: (/ 1 16) #a__U332(x1,x2) weight: 0 a__U326(x1,x2,x3,x4) weight: (/ 1 32) + x1 + x2 U251(x1,x2,x3) weight: (/ 13 32) + x1 + x3 #a__U322(x1,x2,x3,x4) weight: 0 a__isLNatKind(x1) weight: (/ 1 4) + x1 #a__U121(x1,x2) weight: (/ 1 16) U52(x1,x2,x3) weight: (/ 1 2) + x3 #a__U254(x1,x2,x3) weight: (/ 1 8) #a__U324(x1,x2,x3,x4) weight: 0 #a__U281(x1,x2) weight: 0 #a__U251(x1,x2,x3) weight: (/ 7 32) U61(x1,x2) weight: (/ 13 32) + x1 + x2 a__U46(x1) weight: (/ 1 32) + x1 #a__U22(x1,x2,x3) weight: (/ 1 32) a__U13(x1,x2,x3) weight: (/ 7 32) + x2 a__U304(x1,x2) weight: (/ 1 32) + x1 U31(x1,x2,x3) weight: (/ 9 32) + x1 + x2 #a__U83(x1) weight: 0 #a__U171(x1,x2) weight: (/ 1 16) a__U71(x1,x2) weight: (/ 3 8) U183(x1) weight: (/ 3 16) U245(x1,x2) weight: (/ 19 32) + x1 U92(x1,x2) weight: (/ 7 16) + x1 + x2 #a__isPLNat(x1) weight: (/ 1 4) #a__U203(x1,x2,x3) weight: (/ 1 16) head(x1) weight: (/ 1 4) + x1 #a__afterNth(x1,x2) weight: 0 U112(x1) weight: (/ 13 32) + x1 #a__U343(x1,x2,x3) weight: (/ 1 32) #a__splitAt(x1,x2) weight: 0 #a__isPLNatKind(x1) weight: (/ 1 16) #a__U192(x1,x2) weight: (/ 1 32) a__U255(x1,x2) weight: (/ 3 32) + x1 + x2 cons(x1,x2) weight: (/ 1 4) a__U344(x1,x2,x3) weight: (/ 1 32) + x1 + x3 a__U92(x1,x2) weight: (/ 13 32) U323(x1,x2,x3,x4) weight: (/ 3 16) + x1 + x4 a__U61(x1,x2) weight: (/ 3 8) U102(x1,x2,x3) weight: (/ 5 32) a__U105(x1,x2) weight: (/ 7 32) + x2 a__U334(x1,x2) weight: (/ 3 32) + x1 snd(x1) weight: (/ 3 16) + x1 a__take(x1,x2) weight: (/ 1 32) + x1 U256(x1) weight: (/ 3 16) + x1 a__U301(x1,x2,x3) weight: (/ 3 16) + x2 U81(x1,x2) weight: (/ 1 32) + x1 #a__U41(x1,x2,x3) weight: (/ 7 32) U82(x1,x2) weight: (/ 7 16) #a__U304(x1,x2) weight: 0 tt() weight: 0 a__isNatural(x1) weight: (/ 5 32) a__isNaturalKind(x1) weight: (/ 5 32) a__U131(x1) weight: (/ 15 32) #a__isNatural(x1) weight: 0 U13(x1,x2,x3) weight: (/ 1 4) #a__fst(x1) weight: (/ 1 32) a__U23(x1,x2,x3) weight: (/ 1 16) #a__U311(x1,x2) weight: 0 a__U201(x1,x2,x3) weight: (/ 3 16) + x2 #a__U271(x1,x2) weight: (/ 1 16) a__U202(x1,x2,x3) weight: (/ 7 32) + x2 + x3 U321(x1,x2,x3,x4) weight: (/ 7 32) + x1 + x2 + x3 + x4 a__U282(x1,x2) weight: (/ 7 32) #a__U241(x1,x2,x3) weight: (/ 5 32) a__U183(x1) weight: (/ 5 32) a__U333(x1,x2) weight: (/ 1 32) + x1 + x2 U22(x1,x2,x3) weight: (/ 1 16) + x3 #a__U293(x1,x2,x3) weight: (/ 1 32) U51(x1,x2,x3) weight: (/ 15 32) + x2 U311(x1,x2) weight: (/ 7 32) + x1 + x2 #a__U325(x1,x2,x3,x4) weight: 0 #a__U34(x1,x2) weight: 0 U322(x1,x2,x3,x4) weight: (/ 5 32) + x1 + x3 + x4 U344(x1,x2,x3) weight: (/ 1 16) + x2 a__U342(x1,x2,x3) weight: (/ 3 16) + x3 a__tail(x1) weight: (/ 5 32) a__U103(x1,x2,x3) weight: (/ 5 32) a__U54(x1,x2,x3) weight: (/ 17 32) + x3 a__isPLNatKind(x1) weight: (/ 5 32) U53(x1,x2,x3) weight: (/ 17 32) + x2 + x3 a__U303(x1,x2) weight: (/ 1 4) a__U323(x1,x2,x3,x4) weight: (/ 5 32) + x2 #a__U55(x1,x2) weight: (/ 1 32) a__U112(x1) weight: (/ 3 8) #a__U331(x1,x2,x3) weight: (/ 1 32) U41(x1,x2,x3) weight: (/ 9 32) + x1 + x2 #a__tail(x1) weight: (/ 1 32) a__U203(x1,x2,x3) weight: (/ 1 4) #a__U32(x1,x2,x3) weight: (/ 1 32) #a__U221(x1) weight: 0 a__U101(x1,x2,x3) weight: (/ 1 4) #a__U91(x1,x2) weight: (/ 1 16) a__U341(x1,x2,x3) weight: (/ 5 32) U282(x1,x2) weight: (/ 1 4) a__U256(x1) weight: (/ 5 32) U121(x1,x2) weight: (/ 9 16) + x1 a__head(x1) weight: (/ 7 32) U181(x1,x2) weight: (/ 7 32) + x1 U324(x1,x2,x3,x4) weight: (/ 1 16) + x1 U331(x1,x2,x3) weight: (/ 1 16) + x1 + x2 + x3 U122(x1) weight: (/ 19 32) + x1 a__U312(x1,x2) weight: (/ 7 32) + x2 #a__U327(x1,x2) weight: 0 Usable rules: { } Removed DPs: #47 #94 #119 #191 #210 #254 #365 #379 #393 #395 #415 #482 Number of SCCs: 2, DPs: 7, edges: 7 SCC { #52 #70 #72 #80 #88 #171 #292 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS.