Input TRS:
    1: active(U101(tt(),V1,V2)) -> mark(U102(isNaturalKind(V1),V1,V2))
    2: active(U102(tt(),V1,V2)) -> mark(U103(isLNatKind(V2),V1,V2))
    3: active(U103(tt(),V1,V2)) -> mark(U104(isLNatKind(V2),V1,V2))
    4: active(U104(tt(),V1,V2)) -> mark(U105(isNatural(V1),V2))
    5: active(U105(tt(),V2)) -> mark(U106(isLNat(V2)))
    6: active(U106(tt())) -> mark(tt())
    7: active(U11(tt(),N,XS)) -> mark(U12(isNaturalKind(N),N,XS))
    8: active(U111(tt(),V2)) -> mark(U112(isLNatKind(V2)))
    9: active(U112(tt())) -> mark(tt())
    10: active(U12(tt(),N,XS)) -> mark(U13(isLNat(XS),N,XS))
    11: active(U121(tt(),V2)) -> mark(U122(isLNatKind(V2)))
    12: active(U122(tt())) -> mark(tt())
    13: active(U13(tt(),N,XS)) -> mark(U14(isLNatKind(XS),N,XS))
    14: active(U131(tt())) -> mark(tt())
    15: active(U14(tt(),N,XS)) -> mark(snd(splitAt(N,XS)))
    16: active(U141(tt())) -> mark(tt())
    17: active(U151(tt())) -> mark(tt())
    18: active(U161(tt())) -> mark(tt())
    19: active(U171(tt(),V2)) -> mark(U172(isLNatKind(V2)))
    20: active(U172(tt())) -> mark(tt())
    21: active(U181(tt(),V1)) -> mark(U182(isLNatKind(V1),V1))
    22: active(U182(tt(),V1)) -> mark(U183(isLNat(V1)))
    23: active(U183(tt())) -> mark(tt())
    24: active(U191(tt(),V1)) -> mark(U192(isNaturalKind(V1),V1))
    25: active(U192(tt(),V1)) -> mark(U193(isNatural(V1)))
    26: active(U193(tt())) -> mark(tt())
    27: active(U201(tt(),V1,V2)) -> mark(U202(isNaturalKind(V1),V1,V2))
    28: active(U202(tt(),V1,V2)) -> mark(U203(isLNatKind(V2),V1,V2))
    29: active(U203(tt(),V1,V2)) -> mark(U204(isLNatKind(V2),V1,V2))
    30: active(U204(tt(),V1,V2)) -> mark(U205(isNatural(V1),V2))
    31: active(U205(tt(),V2)) -> mark(U206(isLNat(V2)))
    32: active(U206(tt())) -> mark(tt())
    33: active(U21(tt(),X,Y)) -> mark(U22(isLNatKind(X),X,Y))
    34: active(U211(tt())) -> mark(tt())
    35: active(U22(tt(),X,Y)) -> mark(U23(isLNat(Y),X,Y))
    36: active(U221(tt())) -> mark(tt())
    37: active(U23(tt(),X,Y)) -> mark(U24(isLNatKind(Y),X))
    38: active(U231(tt(),V2)) -> mark(U232(isLNatKind(V2)))
    39: active(U232(tt())) -> mark(tt())
    40: active(U24(tt(),X)) -> mark(X)
    41: active(U241(tt(),V1,V2)) -> mark(U242(isLNatKind(V1),V1,V2))
    42: active(U242(tt(),V1,V2)) -> mark(U243(isLNatKind(V2),V1,V2))
    43: active(U243(tt(),V1,V2)) -> mark(U244(isLNatKind(V2),V1,V2))
    44: active(U244(tt(),V1,V2)) -> mark(U245(isLNat(V1),V2))
    45: active(U245(tt(),V2)) -> mark(U246(isLNat(V2)))
    46: active(U246(tt())) -> mark(tt())
    47: active(U251(tt(),V1,V2)) -> mark(U252(isNaturalKind(V1),V1,V2))
    48: active(U252(tt(),V1,V2)) -> mark(U253(isLNatKind(V2),V1,V2))
    49: active(U253(tt(),V1,V2)) -> mark(U254(isLNatKind(V2),V1,V2))
    50: active(U254(tt(),V1,V2)) -> mark(U255(isNatural(V1),V2))
    51: active(U255(tt(),V2)) -> mark(U256(isLNat(V2)))
    52: active(U256(tt())) -> mark(tt())
    53: active(U261(tt(),V2)) -> mark(U262(isLNatKind(V2)))
    54: active(U262(tt())) -> mark(tt())
    55: active(U271(tt(),V2)) -> mark(U272(isLNatKind(V2)))
    56: active(U272(tt())) -> mark(tt())
    57: active(U281(tt(),N)) -> mark(U282(isNaturalKind(N),N))
    58: active(U282(tt(),N)) -> mark(cons(N,natsFrom(s(N))))
    59: active(U291(tt(),N,XS)) -> mark(U292(isNaturalKind(N),N,XS))
    60: active(U292(tt(),N,XS)) -> mark(U293(isLNat(XS),N,XS))
    61: active(U293(tt(),N,XS)) -> mark(U294(isLNatKind(XS),N,XS))
    62: active(U294(tt(),N,XS)) -> mark(head(afterNth(N,XS)))
    63: active(U301(tt(),X,Y)) -> mark(U302(isLNatKind(X),Y))
    64: active(U302(tt(),Y)) -> mark(U303(isLNat(Y),Y))
    65: active(U303(tt(),Y)) -> mark(U304(isLNatKind(Y),Y))
    66: active(U304(tt(),Y)) -> mark(Y)
    67: active(U31(tt(),N,XS)) -> mark(U32(isNaturalKind(N),N,XS))
    68: active(U311(tt(),XS)) -> mark(U312(isLNatKind(XS),XS))
    69: active(U312(tt(),XS)) -> mark(pair(nil(),XS))
    70: active(U32(tt(),N,XS)) -> mark(U33(isLNat(XS),N,XS))
    71: active(U321(tt(),N,X,XS)) -> mark(U322(isNaturalKind(N),N,X,XS))
    72: active(U322(tt(),N,X,XS)) -> mark(U323(isNatural(X),N,X,XS))
    73: active(U323(tt(),N,X,XS)) -> mark(U324(isNaturalKind(X),N,X,XS))
    74: active(U324(tt(),N,X,XS)) -> mark(U325(isLNat(XS),N,X,XS))
    75: active(U325(tt(),N,X,XS)) -> mark(U326(isLNatKind(XS),N,X,XS))
    76: active(U326(tt(),N,X,XS)) -> mark(U327(splitAt(N,XS),X))
    77: active(U327(pair(YS,ZS),X)) -> mark(pair(cons(X,YS),ZS))
    78: active(U33(tt(),N,XS)) -> mark(U34(isLNatKind(XS),N))
    79: active(U331(tt(),N,XS)) -> mark(U332(isNaturalKind(N),XS))
    80: active(U332(tt(),XS)) -> mark(U333(isLNat(XS),XS))
    81: active(U333(tt(),XS)) -> mark(U334(isLNatKind(XS),XS))
    82: active(U334(tt(),XS)) -> mark(XS)
    83: active(U34(tt(),N)) -> mark(N)
    84: active(U341(tt(),N,XS)) -> mark(U342(isNaturalKind(N),N,XS))
    85: active(U342(tt(),N,XS)) -> mark(U343(isLNat(XS),N,XS))
    86: active(U343(tt(),N,XS)) -> mark(U344(isLNatKind(XS),N,XS))
    87: active(U344(tt(),N,XS)) -> mark(fst(splitAt(N,XS)))
    88: active(U41(tt(),V1,V2)) -> mark(U42(isNaturalKind(V1),V1,V2))
    89: active(U42(tt(),V1,V2)) -> mark(U43(isLNatKind(V2),V1,V2))
    90: active(U43(tt(),V1,V2)) -> mark(U44(isLNatKind(V2),V1,V2))
    91: active(U44(tt(),V1,V2)) -> mark(U45(isNatural(V1),V2))
    92: active(U45(tt(),V2)) -> mark(U46(isLNat(V2)))
    93: active(U46(tt())) -> mark(tt())
    94: active(U51(tt(),V1,V2)) -> mark(U52(isNaturalKind(V1),V1,V2))
    95: active(U52(tt(),V1,V2)) -> mark(U53(isLNatKind(V2),V1,V2))
    96: active(U53(tt(),V1,V2)) -> mark(U54(isLNatKind(V2),V1,V2))
    97: active(U54(tt(),V1,V2)) -> mark(U55(isNatural(V1),V2))
    98: active(U55(tt(),V2)) -> mark(U56(isLNat(V2)))
    99: active(U56(tt())) -> mark(tt())
    100: active(U61(tt(),V1)) -> mark(U62(isPLNatKind(V1),V1))
    101: active(U62(tt(),V1)) -> mark(U63(isPLNat(V1)))
    102: active(U63(tt())) -> mark(tt())
    103: active(U71(tt(),V1)) -> mark(U72(isNaturalKind(V1),V1))
    104: active(U72(tt(),V1)) -> mark(U73(isNatural(V1)))
    105: active(U73(tt())) -> mark(tt())
    106: active(U81(tt(),V1)) -> mark(U82(isPLNatKind(V1),V1))
    107: active(U82(tt(),V1)) -> mark(U83(isPLNat(V1)))
    108: active(U83(tt())) -> mark(tt())
    109: active(U91(tt(),V1)) -> mark(U92(isLNatKind(V1),V1))
    110: active(U92(tt(),V1)) -> mark(U93(isLNat(V1)))
    111: active(U93(tt())) -> mark(tt())
    112: active(afterNth(N,XS)) -> mark(U11(isNatural(N),N,XS))
    113: active(fst(pair(X,Y))) -> mark(U21(isLNat(X),X,Y))
    114: active(head(cons(N,XS))) -> mark(U31(isNatural(N),N,XS))
    115: active(isLNat(nil())) -> mark(tt())
    116: active(isLNat(afterNth(V1,V2))) -> mark(U41(isNaturalKind(V1),V1,V2))
    117: active(isLNat(cons(V1,V2))) -> mark(U51(isNaturalKind(V1),V1,V2))
    118: active(isLNat(fst(V1))) -> mark(U61(isPLNatKind(V1),V1))
    119: active(isLNat(natsFrom(V1))) -> mark(U71(isNaturalKind(V1),V1))
    120: active(isLNat(snd(V1))) -> mark(U81(isPLNatKind(V1),V1))
    121: active(isLNat(tail(V1))) -> mark(U91(isLNatKind(V1),V1))
    122: active(isLNat(take(V1,V2))) -> mark(U101(isNaturalKind(V1),V1,V2))
    123: active(isLNatKind(nil())) -> mark(tt())
    124: active(isLNatKind(afterNth(V1,V2))) -> mark(U111(isNaturalKind(V1),V2))
    125: active(isLNatKind(cons(V1,V2))) -> mark(U121(isNaturalKind(V1),V2))
    126: active(isLNatKind(fst(V1))) -> mark(U131(isPLNatKind(V1)))
    127: active(isLNatKind(natsFrom(V1))) -> mark(U141(isNaturalKind(V1)))
    128: active(isLNatKind(snd(V1))) -> mark(U151(isPLNatKind(V1)))
    129: active(isLNatKind(tail(V1))) -> mark(U161(isLNatKind(V1)))
    130: active(isLNatKind(take(V1,V2))) -> mark(U171(isNaturalKind(V1),V2))
    131: active(isNatural(0())) -> mark(tt())
    132: active(isNatural(head(V1))) -> mark(U181(isLNatKind(V1),V1))
    133: active(isNatural(s(V1))) -> mark(U191(isNaturalKind(V1),V1))
    134: active(isNatural(sel(V1,V2))) -> mark(U201(isNaturalKind(V1),V1,V2))
    135: active(isNaturalKind(0())) -> mark(tt())
    136: active(isNaturalKind(head(V1))) -> mark(U211(isLNatKind(V1)))
    137: active(isNaturalKind(s(V1))) -> mark(U221(isNaturalKind(V1)))
    138: active(isNaturalKind(sel(V1,V2))) -> mark(U231(isNaturalKind(V1),V2))
    139: active(isPLNat(pair(V1,V2))) -> mark(U241(isLNatKind(V1),V1,V2))
    140: active(isPLNat(splitAt(V1,V2))) -> mark(U251(isNaturalKind(V1),V1,V2))
    141: active(isPLNatKind(pair(V1,V2))) -> mark(U261(isLNatKind(V1),V2))
    142: active(isPLNatKind(splitAt(V1,V2))) -> mark(U271(isNaturalKind(V1),V2))
    143: active(natsFrom(N)) -> mark(U281(isNatural(N),N))
    144: active(sel(N,XS)) -> mark(U291(isNatural(N),N,XS))
    145: active(snd(pair(X,Y))) -> mark(U301(isLNat(X),X,Y))
    146: active(splitAt(0(),XS)) -> mark(U311(isLNat(XS),XS))
    147: active(splitAt(s(N),cons(X,XS))) -> mark(U321(isNatural(N),N,X,XS))
    148: active(tail(cons(N,XS))) -> mark(U331(isNatural(N),N,XS))
    149: active(take(N,XS)) -> mark(U341(isNatural(N),N,XS))
    150: active(U101(X1,X2,X3)) -> U101(active(X1),X2,X3)
    151: active(U102(X1,X2,X3)) -> U102(active(X1),X2,X3)
    152: active(U103(X1,X2,X3)) -> U103(active(X1),X2,X3)
    153: active(U104(X1,X2,X3)) -> U104(active(X1),X2,X3)
    154: active(U105(X1,X2)) -> U105(active(X1),X2)
    155: active(U106(X)) -> U106(active(X))
    156: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
    157: active(U12(X1,X2,X3)) -> U12(active(X1),X2,X3)
    158: active(U111(X1,X2)) -> U111(active(X1),X2)
    159: active(U112(X)) -> U112(active(X))
    160: active(U13(X1,X2,X3)) -> U13(active(X1),X2,X3)
    161: active(U121(X1,X2)) -> U121(active(X1),X2)
    162: active(U122(X)) -> U122(active(X))
    163: active(U14(X1,X2,X3)) -> U14(active(X1),X2,X3)
    164: active(U131(X)) -> U131(active(X))
    165: active(snd(X)) -> snd(active(X))
    166: active(splitAt(X1,X2)) -> splitAt(active(X1),X2)
    167: active(splitAt(X1,X2)) -> splitAt(X1,active(X2))
    168: active(U141(X)) -> U141(active(X))
    169: active(U151(X)) -> U151(active(X))
    170: active(U161(X)) -> U161(active(X))
    171: active(U171(X1,X2)) -> U171(active(X1),X2)
    172: active(U172(X)) -> U172(active(X))
    173: active(U181(X1,X2)) -> U181(active(X1),X2)
    174: active(U182(X1,X2)) -> U182(active(X1),X2)
    175: active(U183(X)) -> U183(active(X))
    176: active(U191(X1,X2)) -> U191(active(X1),X2)
    177: active(U192(X1,X2)) -> U192(active(X1),X2)
    178: active(U193(X)) -> U193(active(X))
    179: active(U201(X1,X2,X3)) -> U201(active(X1),X2,X3)
    180: active(U202(X1,X2,X3)) -> U202(active(X1),X2,X3)
    181: active(U203(X1,X2,X3)) -> U203(active(X1),X2,X3)
    182: active(U204(X1,X2,X3)) -> U204(active(X1),X2,X3)
    183: active(U205(X1,X2)) -> U205(active(X1),X2)
    184: active(U206(X)) -> U206(active(X))
    185: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
    186: active(U22(X1,X2,X3)) -> U22(active(X1),X2,X3)
    187: active(U211(X)) -> U211(active(X))
    188: active(U23(X1,X2,X3)) -> U23(active(X1),X2,X3)
    189: active(U221(X)) -> U221(active(X))
    190: active(U24(X1,X2)) -> U24(active(X1),X2)
    191: active(U231(X1,X2)) -> U231(active(X1),X2)
    192: active(U232(X)) -> U232(active(X))
    193: active(U241(X1,X2,X3)) -> U241(active(X1),X2,X3)
    194: active(U242(X1,X2,X3)) -> U242(active(X1),X2,X3)
    195: active(U243(X1,X2,X3)) -> U243(active(X1),X2,X3)
    196: active(U244(X1,X2,X3)) -> U244(active(X1),X2,X3)
    197: active(U245(X1,X2)) -> U245(active(X1),X2)
    198: active(U246(X)) -> U246(active(X))
    199: active(U251(X1,X2,X3)) -> U251(active(X1),X2,X3)
    200: active(U252(X1,X2,X3)) -> U252(active(X1),X2,X3)
    201: active(U253(X1,X2,X3)) -> U253(active(X1),X2,X3)
    202: active(U254(X1,X2,X3)) -> U254(active(X1),X2,X3)
    203: active(U255(X1,X2)) -> U255(active(X1),X2)
    204: active(U256(X)) -> U256(active(X))
    205: active(U261(X1,X2)) -> U261(active(X1),X2)
    206: active(U262(X)) -> U262(active(X))
    207: active(U271(X1,X2)) -> U271(active(X1),X2)
    208: active(U272(X)) -> U272(active(X))
    209: active(U281(X1,X2)) -> U281(active(X1),X2)
    210: active(U282(X1,X2)) -> U282(active(X1),X2)
    211: active(cons(X1,X2)) -> cons(active(X1),X2)
    212: active(natsFrom(X)) -> natsFrom(active(X))
    213: active(s(X)) -> s(active(X))
    214: active(U291(X1,X2,X3)) -> U291(active(X1),X2,X3)
    215: active(U292(X1,X2,X3)) -> U292(active(X1),X2,X3)
    216: active(U293(X1,X2,X3)) -> U293(active(X1),X2,X3)
    217: active(U294(X1,X2,X3)) -> U294(active(X1),X2,X3)
    218: active(head(X)) -> head(active(X))
    219: active(afterNth(X1,X2)) -> afterNth(active(X1),X2)
    220: active(afterNth(X1,X2)) -> afterNth(X1,active(X2))
    221: active(U301(X1,X2,X3)) -> U301(active(X1),X2,X3)
    222: active(U302(X1,X2)) -> U302(active(X1),X2)
    223: active(U303(X1,X2)) -> U303(active(X1),X2)
    224: active(U304(X1,X2)) -> U304(active(X1),X2)
    225: active(U31(X1,X2,X3)) -> U31(active(X1),X2,X3)
    226: active(U32(X1,X2,X3)) -> U32(active(X1),X2,X3)
    227: active(U311(X1,X2)) -> U311(active(X1),X2)
    228: active(U312(X1,X2)) -> U312(active(X1),X2)
    229: active(pair(X1,X2)) -> pair(active(X1),X2)
    230: active(pair(X1,X2)) -> pair(X1,active(X2))
    231: active(U33(X1,X2,X3)) -> U33(active(X1),X2,X3)
    232: active(U321(X1,X2,X3,X4)) -> U321(active(X1),X2,X3,X4)
    233: active(U322(X1,X2,X3,X4)) -> U322(active(X1),X2,X3,X4)
    234: active(U323(X1,X2,X3,X4)) -> U323(active(X1),X2,X3,X4)
    235: active(U324(X1,X2,X3,X4)) -> U324(active(X1),X2,X3,X4)
    236: active(U325(X1,X2,X3,X4)) -> U325(active(X1),X2,X3,X4)
    237: active(U326(X1,X2,X3,X4)) -> U326(active(X1),X2,X3,X4)
    238: active(U327(X1,X2)) -> U327(active(X1),X2)
    239: active(U34(X1,X2)) -> U34(active(X1),X2)
    240: active(U331(X1,X2,X3)) -> U331(active(X1),X2,X3)
    241: active(U332(X1,X2)) -> U332(active(X1),X2)
    242: active(U333(X1,X2)) -> U333(active(X1),X2)
    243: active(U334(X1,X2)) -> U334(active(X1),X2)
    244: active(U341(X1,X2,X3)) -> U341(active(X1),X2,X3)
    245: active(U342(X1,X2,X3)) -> U342(active(X1),X2,X3)
    246: active(U343(X1,X2,X3)) -> U343(active(X1),X2,X3)
    247: active(U344(X1,X2,X3)) -> U344(active(X1),X2,X3)
    248: active(fst(X)) -> fst(active(X))
    249: active(U41(X1,X2,X3)) -> U41(active(X1),X2,X3)
    250: active(U42(X1,X2,X3)) -> U42(active(X1),X2,X3)
    251: active(U43(X1,X2,X3)) -> U43(active(X1),X2,X3)
    252: active(U44(X1,X2,X3)) -> U44(active(X1),X2,X3)
    253: active(U45(X1,X2)) -> U45(active(X1),X2)
    254: active(U46(X)) -> U46(active(X))
    255: active(U51(X1,X2,X3)) -> U51(active(X1),X2,X3)
    256: active(U52(X1,X2,X3)) -> U52(active(X1),X2,X3)
    257: active(U53(X1,X2,X3)) -> U53(active(X1),X2,X3)
    258: active(U54(X1,X2,X3)) -> U54(active(X1),X2,X3)
    259: active(U55(X1,X2)) -> U55(active(X1),X2)
    260: active(U56(X)) -> U56(active(X))
    261: active(U61(X1,X2)) -> U61(active(X1),X2)
    262: active(U62(X1,X2)) -> U62(active(X1),X2)
    263: active(U63(X)) -> U63(active(X))
    264: active(U71(X1,X2)) -> U71(active(X1),X2)
    265: active(U72(X1,X2)) -> U72(active(X1),X2)
    266: active(U73(X)) -> U73(active(X))
    267: active(U81(X1,X2)) -> U81(active(X1),X2)
    268: active(U82(X1,X2)) -> U82(active(X1),X2)
    269: active(U83(X)) -> U83(active(X))
    270: active(U91(X1,X2)) -> U91(active(X1),X2)
    271: active(U92(X1,X2)) -> U92(active(X1),X2)
    272: active(U93(X)) -> U93(active(X))
    273: active(tail(X)) -> tail(active(X))
    274: active(take(X1,X2)) -> take(active(X1),X2)
    275: active(take(X1,X2)) -> take(X1,active(X2))
    276: active(sel(X1,X2)) -> sel(active(X1),X2)
    277: active(sel(X1,X2)) -> sel(X1,active(X2))
    278: U101(mark(X1),X2,X3) -> mark(U101(X1,X2,X3))
    279: U102(mark(X1),X2,X3) -> mark(U102(X1,X2,X3))
    280: U103(mark(X1),X2,X3) -> mark(U103(X1,X2,X3))
    281: U104(mark(X1),X2,X3) -> mark(U104(X1,X2,X3))
    282: U105(mark(X1),X2) -> mark(U105(X1,X2))
    283: U106(mark(X)) -> mark(U106(X))
    284: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
    285: U12(mark(X1),X2,X3) -> mark(U12(X1,X2,X3))
    286: U111(mark(X1),X2) -> mark(U111(X1,X2))
    287: U112(mark(X)) -> mark(U112(X))
    288: U13(mark(X1),X2,X3) -> mark(U13(X1,X2,X3))
    289: U121(mark(X1),X2) -> mark(U121(X1,X2))
    290: U122(mark(X)) -> mark(U122(X))
    291: U14(mark(X1),X2,X3) -> mark(U14(X1,X2,X3))
    292: U131(mark(X)) -> mark(U131(X))
    293: snd(mark(X)) -> mark(snd(X))
    294: splitAt(mark(X1),X2) -> mark(splitAt(X1,X2))
    295: splitAt(X1,mark(X2)) -> mark(splitAt(X1,X2))
    296: U141(mark(X)) -> mark(U141(X))
    297: U151(mark(X)) -> mark(U151(X))
    298: U161(mark(X)) -> mark(U161(X))
    299: U171(mark(X1),X2) -> mark(U171(X1,X2))
    300: U172(mark(X)) -> mark(U172(X))
    301: U181(mark(X1),X2) -> mark(U181(X1,X2))
    302: U182(mark(X1),X2) -> mark(U182(X1,X2))
    303: U183(mark(X)) -> mark(U183(X))
    304: U191(mark(X1),X2) -> mark(U191(X1,X2))
    305: U192(mark(X1),X2) -> mark(U192(X1,X2))
    306: U193(mark(X)) -> mark(U193(X))
    307: U201(mark(X1),X2,X3) -> mark(U201(X1,X2,X3))
    308: U202(mark(X1),X2,X3) -> mark(U202(X1,X2,X3))
    309: U203(mark(X1),X2,X3) -> mark(U203(X1,X2,X3))
    310: U204(mark(X1),X2,X3) -> mark(U204(X1,X2,X3))
    311: U205(mark(X1),X2) -> mark(U205(X1,X2))
    312: U206(mark(X)) -> mark(U206(X))
    313: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
    314: U22(mark(X1),X2,X3) -> mark(U22(X1,X2,X3))
    315: U211(mark(X)) -> mark(U211(X))
    316: U23(mark(X1),X2,X3) -> mark(U23(X1,X2,X3))
    317: U221(mark(X)) -> mark(U221(X))
    318: U24(mark(X1),X2) -> mark(U24(X1,X2))
    319: U231(mark(X1),X2) -> mark(U231(X1,X2))
    320: U232(mark(X)) -> mark(U232(X))
    321: U241(mark(X1),X2,X3) -> mark(U241(X1,X2,X3))
    322: U242(mark(X1),X2,X3) -> mark(U242(X1,X2,X3))
    323: U243(mark(X1),X2,X3) -> mark(U243(X1,X2,X3))
    324: U244(mark(X1),X2,X3) -> mark(U244(X1,X2,X3))
    325: U245(mark(X1),X2) -> mark(U245(X1,X2))
    326: U246(mark(X)) -> mark(U246(X))
    327: U251(mark(X1),X2,X3) -> mark(U251(X1,X2,X3))
    328: U252(mark(X1),X2,X3) -> mark(U252(X1,X2,X3))
    329: U253(mark(X1),X2,X3) -> mark(U253(X1,X2,X3))
    330: U254(mark(X1),X2,X3) -> mark(U254(X1,X2,X3))
    331: U255(mark(X1),X2) -> mark(U255(X1,X2))
    332: U256(mark(X)) -> mark(U256(X))
    333: U261(mark(X1),X2) -> mark(U261(X1,X2))
    334: U262(mark(X)) -> mark(U262(X))
    335: U271(mark(X1),X2) -> mark(U271(X1,X2))
    336: U272(mark(X)) -> mark(U272(X))
    337: U281(mark(X1),X2) -> mark(U281(X1,X2))
    338: U282(mark(X1),X2) -> mark(U282(X1,X2))
    339: cons(mark(X1),X2) -> mark(cons(X1,X2))
    340: natsFrom(mark(X)) -> mark(natsFrom(X))
    341: s(mark(X)) -> mark(s(X))
    342: U291(mark(X1),X2,X3) -> mark(U291(X1,X2,X3))
    343: U292(mark(X1),X2,X3) -> mark(U292(X1,X2,X3))
    344: U293(mark(X1),X2,X3) -> mark(U293(X1,X2,X3))
    345: U294(mark(X1),X2,X3) -> mark(U294(X1,X2,X3))
    346: head(mark(X)) -> mark(head(X))
    347: afterNth(mark(X1),X2) -> mark(afterNth(X1,X2))
    348: afterNth(X1,mark(X2)) -> mark(afterNth(X1,X2))
    349: U301(mark(X1),X2,X3) -> mark(U301(X1,X2,X3))
    350: U302(mark(X1),X2) -> mark(U302(X1,X2))
    351: U303(mark(X1),X2) -> mark(U303(X1,X2))
    352: U304(mark(X1),X2) -> mark(U304(X1,X2))
    353: U31(mark(X1),X2,X3) -> mark(U31(X1,X2,X3))
    354: U32(mark(X1),X2,X3) -> mark(U32(X1,X2,X3))
    355: U311(mark(X1),X2) -> mark(U311(X1,X2))
    356: U312(mark(X1),X2) -> mark(U312(X1,X2))
    357: pair(mark(X1),X2) -> mark(pair(X1,X2))
    358: pair(X1,mark(X2)) -> mark(pair(X1,X2))
    359: U33(mark(X1),X2,X3) -> mark(U33(X1,X2,X3))
    360: U321(mark(X1),X2,X3,X4) -> mark(U321(X1,X2,X3,X4))
    361: U322(mark(X1),X2,X3,X4) -> mark(U322(X1,X2,X3,X4))
    362: U323(mark(X1),X2,X3,X4) -> mark(U323(X1,X2,X3,X4))
    363: U324(mark(X1),X2,X3,X4) -> mark(U324(X1,X2,X3,X4))
    364: U325(mark(X1),X2,X3,X4) -> mark(U325(X1,X2,X3,X4))
    365: U326(mark(X1),X2,X3,X4) -> mark(U326(X1,X2,X3,X4))
    366: U327(mark(X1),X2) -> mark(U327(X1,X2))
    367: U34(mark(X1),X2) -> mark(U34(X1,X2))
    368: U331(mark(X1),X2,X3) -> mark(U331(X1,X2,X3))
    369: U332(mark(X1),X2) -> mark(U332(X1,X2))
    370: U333(mark(X1),X2) -> mark(U333(X1,X2))
    371: U334(mark(X1),X2) -> mark(U334(X1,X2))
    372: U341(mark(X1),X2,X3) -> mark(U341(X1,X2,X3))
    373: U342(mark(X1),X2,X3) -> mark(U342(X1,X2,X3))
    374: U343(mark(X1),X2,X3) -> mark(U343(X1,X2,X3))
    375: U344(mark(X1),X2,X3) -> mark(U344(X1,X2,X3))
    376: fst(mark(X)) -> mark(fst(X))
    377: U41(mark(X1),X2,X3) -> mark(U41(X1,X2,X3))
    378: U42(mark(X1),X2,X3) -> mark(U42(X1,X2,X3))
    379: U43(mark(X1),X2,X3) -> mark(U43(X1,X2,X3))
    380: U44(mark(X1),X2,X3) -> mark(U44(X1,X2,X3))
    381: U45(mark(X1),X2) -> mark(U45(X1,X2))
    382: U46(mark(X)) -> mark(U46(X))
    383: U51(mark(X1),X2,X3) -> mark(U51(X1,X2,X3))
    384: U52(mark(X1),X2,X3) -> mark(U52(X1,X2,X3))
    385: U53(mark(X1),X2,X3) -> mark(U53(X1,X2,X3))
    386: U54(mark(X1),X2,X3) -> mark(U54(X1,X2,X3))
    387: U55(mark(X1),X2) -> mark(U55(X1,X2))
    388: U56(mark(X)) -> mark(U56(X))
    389: U61(mark(X1),X2) -> mark(U61(X1,X2))
    390: U62(mark(X1),X2) -> mark(U62(X1,X2))
    391: U63(mark(X)) -> mark(U63(X))
    392: U71(mark(X1),X2) -> mark(U71(X1,X2))
    393: U72(mark(X1),X2) -> mark(U72(X1,X2))
    394: U73(mark(X)) -> mark(U73(X))
    395: U81(mark(X1),X2) -> mark(U81(X1,X2))
    396: U82(mark(X1),X2) -> mark(U82(X1,X2))
    397: U83(mark(X)) -> mark(U83(X))
    398: U91(mark(X1),X2) -> mark(U91(X1,X2))
    399: U92(mark(X1),X2) -> mark(U92(X1,X2))
    400: U93(mark(X)) -> mark(U93(X))
    401: tail(mark(X)) -> mark(tail(X))
    402: take(mark(X1),X2) -> mark(take(X1,X2))
    403: take(X1,mark(X2)) -> mark(take(X1,X2))
    404: sel(mark(X1),X2) -> mark(sel(X1,X2))
    405: sel(X1,mark(X2)) -> mark(sel(X1,X2))
    406: proper(U101(X1,X2,X3)) -> U101(proper(X1),proper(X2),proper(X3))
    407: proper(tt()) -> ok(tt())
    408: proper(U102(X1,X2,X3)) -> U102(proper(X1),proper(X2),proper(X3))
    409: proper(isNaturalKind(X)) -> isNaturalKind(proper(X))
    410: proper(U103(X1,X2,X3)) -> U103(proper(X1),proper(X2),proper(X3))
    411: proper(isLNatKind(X)) -> isLNatKind(proper(X))
    412: proper(U104(X1,X2,X3)) -> U104(proper(X1),proper(X2),proper(X3))
    413: proper(U105(X1,X2)) -> U105(proper(X1),proper(X2))
    414: proper(isNatural(X)) -> isNatural(proper(X))
    415: proper(U106(X)) -> U106(proper(X))
    416: proper(isLNat(X)) -> isLNat(proper(X))
    417: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
    418: proper(U12(X1,X2,X3)) -> U12(proper(X1),proper(X2),proper(X3))
    419: proper(U111(X1,X2)) -> U111(proper(X1),proper(X2))
    420: proper(U112(X)) -> U112(proper(X))
    421: proper(U13(X1,X2,X3)) -> U13(proper(X1),proper(X2),proper(X3))
    422: proper(U121(X1,X2)) -> U121(proper(X1),proper(X2))
    423: proper(U122(X)) -> U122(proper(X))
    424: proper(U14(X1,X2,X3)) -> U14(proper(X1),proper(X2),proper(X3))
    425: proper(U131(X)) -> U131(proper(X))
    426: proper(snd(X)) -> snd(proper(X))
    427: proper(splitAt(X1,X2)) -> splitAt(proper(X1),proper(X2))
    428: proper(U141(X)) -> U141(proper(X))
    429: proper(U151(X)) -> U151(proper(X))
    430: proper(U161(X)) -> U161(proper(X))
    431: proper(U171(X1,X2)) -> U171(proper(X1),proper(X2))
    432: proper(U172(X)) -> U172(proper(X))
    433: proper(U181(X1,X2)) -> U181(proper(X1),proper(X2))
    434: proper(U182(X1,X2)) -> U182(proper(X1),proper(X2))
    435: proper(U183(X)) -> U183(proper(X))
    436: proper(U191(X1,X2)) -> U191(proper(X1),proper(X2))
    437: proper(U192(X1,X2)) -> U192(proper(X1),proper(X2))
    438: proper(U193(X)) -> U193(proper(X))
    439: proper(U201(X1,X2,X3)) -> U201(proper(X1),proper(X2),proper(X3))
    440: proper(U202(X1,X2,X3)) -> U202(proper(X1),proper(X2),proper(X3))
    441: proper(U203(X1,X2,X3)) -> U203(proper(X1),proper(X2),proper(X3))
    442: proper(U204(X1,X2,X3)) -> U204(proper(X1),proper(X2),proper(X3))
    443: proper(U205(X1,X2)) -> U205(proper(X1),proper(X2))
    444: proper(U206(X)) -> U206(proper(X))
    445: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
    446: proper(U22(X1,X2,X3)) -> U22(proper(X1),proper(X2),proper(X3))
    447: proper(U211(X)) -> U211(proper(X))
    448: proper(U23(X1,X2,X3)) -> U23(proper(X1),proper(X2),proper(X3))
    449: proper(U221(X)) -> U221(proper(X))
    450: proper(U24(X1,X2)) -> U24(proper(X1),proper(X2))
    451: proper(U231(X1,X2)) -> U231(proper(X1),proper(X2))
    452: proper(U232(X)) -> U232(proper(X))
    453: proper(U241(X1,X2,X3)) -> U241(proper(X1),proper(X2),proper(X3))
    454: proper(U242(X1,X2,X3)) -> U242(proper(X1),proper(X2),proper(X3))
    455: proper(U243(X1,X2,X3)) -> U243(proper(X1),proper(X2),proper(X3))
    456: proper(U244(X1,X2,X3)) -> U244(proper(X1),proper(X2),proper(X3))
    457: proper(U245(X1,X2)) -> U245(proper(X1),proper(X2))
    458: proper(U246(X)) -> U246(proper(X))
    459: proper(U251(X1,X2,X3)) -> U251(proper(X1),proper(X2),proper(X3))
    460: proper(U252(X1,X2,X3)) -> U252(proper(X1),proper(X2),proper(X3))
    461: proper(U253(X1,X2,X3)) -> U253(proper(X1),proper(X2),proper(X3))
    462: proper(U254(X1,X2,X3)) -> U254(proper(X1),proper(X2),proper(X3))
    463: proper(U255(X1,X2)) -> U255(proper(X1),proper(X2))
    464: proper(U256(X)) -> U256(proper(X))
    465: proper(U261(X1,X2)) -> U261(proper(X1),proper(X2))
    466: proper(U262(X)) -> U262(proper(X))
    467: proper(U271(X1,X2)) -> U271(proper(X1),proper(X2))
    468: proper(U272(X)) -> U272(proper(X))
    469: proper(U281(X1,X2)) -> U281(proper(X1),proper(X2))
    470: proper(U282(X1,X2)) -> U282(proper(X1),proper(X2))
    471: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    472: proper(natsFrom(X)) -> natsFrom(proper(X))
    473: proper(s(X)) -> s(proper(X))
    474: proper(U291(X1,X2,X3)) -> U291(proper(X1),proper(X2),proper(X3))
    475: proper(U292(X1,X2,X3)) -> U292(proper(X1),proper(X2),proper(X3))
    476: proper(U293(X1,X2,X3)) -> U293(proper(X1),proper(X2),proper(X3))
    477: proper(U294(X1,X2,X3)) -> U294(proper(X1),proper(X2),proper(X3))
    478: proper(head(X)) -> head(proper(X))
    479: proper(afterNth(X1,X2)) -> afterNth(proper(X1),proper(X2))
    480: proper(U301(X1,X2,X3)) -> U301(proper(X1),proper(X2),proper(X3))
    481: proper(U302(X1,X2)) -> U302(proper(X1),proper(X2))
    482: proper(U303(X1,X2)) -> U303(proper(X1),proper(X2))
    483: proper(U304(X1,X2)) -> U304(proper(X1),proper(X2))
    484: proper(U31(X1,X2,X3)) -> U31(proper(X1),proper(X2),proper(X3))
    485: proper(U32(X1,X2,X3)) -> U32(proper(X1),proper(X2),proper(X3))
    486: proper(U311(X1,X2)) -> U311(proper(X1),proper(X2))
    487: proper(U312(X1,X2)) -> U312(proper(X1),proper(X2))
    488: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
    489: proper(nil()) -> ok(nil())
    490: proper(U33(X1,X2,X3)) -> U33(proper(X1),proper(X2),proper(X3))
    491: proper(U321(X1,X2,X3,X4)) -> U321(proper(X1),proper(X2),proper(X3),proper(X4))
    492: proper(U322(X1,X2,X3,X4)) -> U322(proper(X1),proper(X2),proper(X3),proper(X4))
    493: proper(U323(X1,X2,X3,X4)) -> U323(proper(X1),proper(X2),proper(X3),proper(X4))
    494: proper(U324(X1,X2,X3,X4)) -> U324(proper(X1),proper(X2),proper(X3),proper(X4))
    495: proper(U325(X1,X2,X3,X4)) -> U325(proper(X1),proper(X2),proper(X3),proper(X4))
    496: proper(U326(X1,X2,X3,X4)) -> U326(proper(X1),proper(X2),proper(X3),proper(X4))
    497: proper(U327(X1,X2)) -> U327(proper(X1),proper(X2))
    498: proper(U34(X1,X2)) -> U34(proper(X1),proper(X2))
    499: proper(U331(X1,X2,X3)) -> U331(proper(X1),proper(X2),proper(X3))
    500: proper(U332(X1,X2)) -> U332(proper(X1),proper(X2))
    501: proper(U333(X1,X2)) -> U333(proper(X1),proper(X2))
    502: proper(U334(X1,X2)) -> U334(proper(X1),proper(X2))
    503: proper(U341(X1,X2,X3)) -> U341(proper(X1),proper(X2),proper(X3))
    504: proper(U342(X1,X2,X3)) -> U342(proper(X1),proper(X2),proper(X3))
    505: proper(U343(X1,X2,X3)) -> U343(proper(X1),proper(X2),proper(X3))
    506: proper(U344(X1,X2,X3)) -> U344(proper(X1),proper(X2),proper(X3))
    507: proper(fst(X)) -> fst(proper(X))
    508: proper(U41(X1,X2,X3)) -> U41(proper(X1),proper(X2),proper(X3))
    509: proper(U42(X1,X2,X3)) -> U42(proper(X1),proper(X2),proper(X3))
    510: proper(U43(X1,X2,X3)) -> U43(proper(X1),proper(X2),proper(X3))
    511: proper(U44(X1,X2,X3)) -> U44(proper(X1),proper(X2),proper(X3))
    512: proper(U45(X1,X2)) -> U45(proper(X1),proper(X2))
    513: proper(U46(X)) -> U46(proper(X))
    514: proper(U51(X1,X2,X3)) -> U51(proper(X1),proper(X2),proper(X3))
    515: proper(U52(X1,X2,X3)) -> U52(proper(X1),proper(X2),proper(X3))
    516: proper(U53(X1,X2,X3)) -> U53(proper(X1),proper(X2),proper(X3))
    517: proper(U54(X1,X2,X3)) -> U54(proper(X1),proper(X2),proper(X3))
    518: proper(U55(X1,X2)) -> U55(proper(X1),proper(X2))
    519: proper(U56(X)) -> U56(proper(X))
    520: proper(U61(X1,X2)) -> U61(proper(X1),proper(X2))
    521: proper(U62(X1,X2)) -> U62(proper(X1),proper(X2))
    522: proper(isPLNatKind(X)) -> isPLNatKind(proper(X))
    523: proper(U63(X)) -> U63(proper(X))
    524: proper(isPLNat(X)) -> isPLNat(proper(X))
    525: proper(U71(X1,X2)) -> U71(proper(X1),proper(X2))
    526: proper(U72(X1,X2)) -> U72(proper(X1),proper(X2))
    527: proper(U73(X)) -> U73(proper(X))
    528: proper(U81(X1,X2)) -> U81(proper(X1),proper(X2))
    529: proper(U82(X1,X2)) -> U82(proper(X1),proper(X2))
    530: proper(U83(X)) -> U83(proper(X))
    531: proper(U91(X1,X2)) -> U91(proper(X1),proper(X2))
    532: proper(U92(X1,X2)) -> U92(proper(X1),proper(X2))
    533: proper(U93(X)) -> U93(proper(X))
    534: proper(tail(X)) -> tail(proper(X))
    535: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
    536: proper(0()) -> ok(0())
    537: proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
    538: U101(ok(X1),ok(X2),ok(X3)) -> ok(U101(X1,X2,X3))
    539: U102(ok(X1),ok(X2),ok(X3)) -> ok(U102(X1,X2,X3))
    540: isNaturalKind(ok(X)) -> ok(isNaturalKind(X))
    541: U103(ok(X1),ok(X2),ok(X3)) -> ok(U103(X1,X2,X3))
    542: isLNatKind(ok(X)) -> ok(isLNatKind(X))
    543: U104(ok(X1),ok(X2),ok(X3)) -> ok(U104(X1,X2,X3))
    544: U105(ok(X1),ok(X2)) -> ok(U105(X1,X2))
    545: isNatural(ok(X)) -> ok(isNatural(X))
    546: U106(ok(X)) -> ok(U106(X))
    547: isLNat(ok(X)) -> ok(isLNat(X))
    548: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
    549: U12(ok(X1),ok(X2),ok(X3)) -> ok(U12(X1,X2,X3))
    550: U111(ok(X1),ok(X2)) -> ok(U111(X1,X2))
    551: U112(ok(X)) -> ok(U112(X))
    552: U13(ok(X1),ok(X2),ok(X3)) -> ok(U13(X1,X2,X3))
    553: U121(ok(X1),ok(X2)) -> ok(U121(X1,X2))
    554: U122(ok(X)) -> ok(U122(X))
    555: U14(ok(X1),ok(X2),ok(X3)) -> ok(U14(X1,X2,X3))
    556: U131(ok(X)) -> ok(U131(X))
    557: snd(ok(X)) -> ok(snd(X))
    558: splitAt(ok(X1),ok(X2)) -> ok(splitAt(X1,X2))
    559: U141(ok(X)) -> ok(U141(X))
    560: U151(ok(X)) -> ok(U151(X))
    561: U161(ok(X)) -> ok(U161(X))
    562: U171(ok(X1),ok(X2)) -> ok(U171(X1,X2))
    563: U172(ok(X)) -> ok(U172(X))
    564: U181(ok(X1),ok(X2)) -> ok(U181(X1,X2))
    565: U182(ok(X1),ok(X2)) -> ok(U182(X1,X2))
    566: U183(ok(X)) -> ok(U183(X))
    567: U191(ok(X1),ok(X2)) -> ok(U191(X1,X2))
    568: U192(ok(X1),ok(X2)) -> ok(U192(X1,X2))
    569: U193(ok(X)) -> ok(U193(X))
    570: U201(ok(X1),ok(X2),ok(X3)) -> ok(U201(X1,X2,X3))
    571: U202(ok(X1),ok(X2),ok(X3)) -> ok(U202(X1,X2,X3))
    572: U203(ok(X1),ok(X2),ok(X3)) -> ok(U203(X1,X2,X3))
    573: U204(ok(X1),ok(X2),ok(X3)) -> ok(U204(X1,X2,X3))
    574: U205(ok(X1),ok(X2)) -> ok(U205(X1,X2))
    575: U206(ok(X)) -> ok(U206(X))
    576: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
    577: U22(ok(X1),ok(X2),ok(X3)) -> ok(U22(X1,X2,X3))
    578: U211(ok(X)) -> ok(U211(X))
    579: U23(ok(X1),ok(X2),ok(X3)) -> ok(U23(X1,X2,X3))
    580: U221(ok(X)) -> ok(U221(X))
    581: U24(ok(X1),ok(X2)) -> ok(U24(X1,X2))
    582: U231(ok(X1),ok(X2)) -> ok(U231(X1,X2))
    583: U232(ok(X)) -> ok(U232(X))
    584: U241(ok(X1),ok(X2),ok(X3)) -> ok(U241(X1,X2,X3))
    585: U242(ok(X1),ok(X2),ok(X3)) -> ok(U242(X1,X2,X3))
    586: U243(ok(X1),ok(X2),ok(X3)) -> ok(U243(X1,X2,X3))
    587: U244(ok(X1),ok(X2),ok(X3)) -> ok(U244(X1,X2,X3))
    588: U245(ok(X1),ok(X2)) -> ok(U245(X1,X2))
    589: U246(ok(X)) -> ok(U246(X))
    590: U251(ok(X1),ok(X2),ok(X3)) -> ok(U251(X1,X2,X3))
    591: U252(ok(X1),ok(X2),ok(X3)) -> ok(U252(X1,X2,X3))
    592: U253(ok(X1),ok(X2),ok(X3)) -> ok(U253(X1,X2,X3))
    593: U254(ok(X1),ok(X2),ok(X3)) -> ok(U254(X1,X2,X3))
    594: U255(ok(X1),ok(X2)) -> ok(U255(X1,X2))
    595: U256(ok(X)) -> ok(U256(X))
    596: U261(ok(X1),ok(X2)) -> ok(U261(X1,X2))
    597: U262(ok(X)) -> ok(U262(X))
    598: U271(ok(X1),ok(X2)) -> ok(U271(X1,X2))
    599: U272(ok(X)) -> ok(U272(X))
    600: U281(ok(X1),ok(X2)) -> ok(U281(X1,X2))
    601: U282(ok(X1),ok(X2)) -> ok(U282(X1,X2))
    602: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    603: natsFrom(ok(X)) -> ok(natsFrom(X))
    604: s(ok(X)) -> ok(s(X))
    605: U291(ok(X1),ok(X2),ok(X3)) -> ok(U291(X1,X2,X3))
    606: U292(ok(X1),ok(X2),ok(X3)) -> ok(U292(X1,X2,X3))
    607: U293(ok(X1),ok(X2),ok(X3)) -> ok(U293(X1,X2,X3))
    608: U294(ok(X1),ok(X2),ok(X3)) -> ok(U294(X1,X2,X3))
    609: head(ok(X)) -> ok(head(X))
    610: afterNth(ok(X1),ok(X2)) -> ok(afterNth(X1,X2))
    611: U301(ok(X1),ok(X2),ok(X3)) -> ok(U301(X1,X2,X3))
    612: U302(ok(X1),ok(X2)) -> ok(U302(X1,X2))
    613: U303(ok(X1),ok(X2)) -> ok(U303(X1,X2))
    614: U304(ok(X1),ok(X2)) -> ok(U304(X1,X2))
    615: U31(ok(X1),ok(X2),ok(X3)) -> ok(U31(X1,X2,X3))
    616: U32(ok(X1),ok(X2),ok(X3)) -> ok(U32(X1,X2,X3))
    617: U311(ok(X1),ok(X2)) -> ok(U311(X1,X2))
    618: U312(ok(X1),ok(X2)) -> ok(U312(X1,X2))
    619: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
    620: U33(ok(X1),ok(X2),ok(X3)) -> ok(U33(X1,X2,X3))
    621: U321(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U321(X1,X2,X3,X4))
    622: U322(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U322(X1,X2,X3,X4))
    623: U323(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U323(X1,X2,X3,X4))
    624: U324(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U324(X1,X2,X3,X4))
    625: U325(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U325(X1,X2,X3,X4))
    626: U326(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(U326(X1,X2,X3,X4))
    627: U327(ok(X1),ok(X2)) -> ok(U327(X1,X2))
    628: U34(ok(X1),ok(X2)) -> ok(U34(X1,X2))
    629: U331(ok(X1),ok(X2),ok(X3)) -> ok(U331(X1,X2,X3))
    630: U332(ok(X1),ok(X2)) -> ok(U332(X1,X2))
    631: U333(ok(X1),ok(X2)) -> ok(U333(X1,X2))
    632: U334(ok(X1),ok(X2)) -> ok(U334(X1,X2))
    633: U341(ok(X1),ok(X2),ok(X3)) -> ok(U341(X1,X2,X3))
    634: U342(ok(X1),ok(X2),ok(X3)) -> ok(U342(X1,X2,X3))
    635: U343(ok(X1),ok(X2),ok(X3)) -> ok(U343(X1,X2,X3))
    636: U344(ok(X1),ok(X2),ok(X3)) -> ok(U344(X1,X2,X3))
    637: fst(ok(X)) -> ok(fst(X))
    638: U41(ok(X1),ok(X2),ok(X3)) -> ok(U41(X1,X2,X3))
    639: U42(ok(X1),ok(X2),ok(X3)) -> ok(U42(X1,X2,X3))
    640: U43(ok(X1),ok(X2),ok(X3)) -> ok(U43(X1,X2,X3))
    641: U44(ok(X1),ok(X2),ok(X3)) -> ok(U44(X1,X2,X3))
    642: U45(ok(X1),ok(X2)) -> ok(U45(X1,X2))
    643: U46(ok(X)) -> ok(U46(X))
    644: U51(ok(X1),ok(X2),ok(X3)) -> ok(U51(X1,X2,X3))
    645: U52(ok(X1),ok(X2),ok(X3)) -> ok(U52(X1,X2,X3))
    646: U53(ok(X1),ok(X2),ok(X3)) -> ok(U53(X1,X2,X3))
    647: U54(ok(X1),ok(X2),ok(X3)) -> ok(U54(X1,X2,X3))
    648: U55(ok(X1),ok(X2)) -> ok(U55(X1,X2))
    649: U56(ok(X)) -> ok(U56(X))
    650: U61(ok(X1),ok(X2)) -> ok(U61(X1,X2))
    651: U62(ok(X1),ok(X2)) -> ok(U62(X1,X2))
    652: isPLNatKind(ok(X)) -> ok(isPLNatKind(X))
    653: U63(ok(X)) -> ok(U63(X))
    654: isPLNat(ok(X)) -> ok(isPLNat(X))
    655: U71(ok(X1),ok(X2)) -> ok(U71(X1,X2))
    656: U72(ok(X1),ok(X2)) -> ok(U72(X1,X2))
    657: U73(ok(X)) -> ok(U73(X))
    658: U81(ok(X1),ok(X2)) -> ok(U81(X1,X2))
    659: U82(ok(X1),ok(X2)) -> ok(U82(X1,X2))
    660: U83(ok(X)) -> ok(U83(X))
    661: U91(ok(X1),ok(X2)) -> ok(U91(X1,X2))
    662: U92(ok(X1),ok(X2)) -> ok(U92(X1,X2))
    663: U93(ok(X)) -> ok(U93(X))
    664: tail(ok(X)) -> ok(tail(X))
    665: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
    666: sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
    667: top(mark(X)) -> top(proper(X))
    668: top(ok(X)) -> top(active(X))
Number of strict rules: 668
Direct Order(PosReal,>,Poly) ...