Problem Transformed CSR 04 LISTUTILITIES complete-noand L

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 LISTUTILITIES complete-noand L

stdout:

MAYBE
The following error occured:
The problem does not contain well-formed TRSs:

                                                REWRITE relation according to the following TRS
                                                 {  U14(tt()) -> snd(splitAt(N, XS))
                                                  , U24(tt()) -> X
                                                  , U282(tt()) -> cons(N)
                                                  , U294(tt()) -> head(afterNth(N, XS))
                                                  , U304(tt()) -> Y
                                                  , U312(tt()) -> pair(nil(), XS)
                                                  , U326(tt()) -> U327(splitAt(N, XS))
                                                  , U327(pair(YS, ZS)) -> pair(cons(X), ZS)
                                                  , U334(tt()) -> XS
                                                  , U34(tt()) -> N
                                                  , U344(tt()) -> fst(splitAt(N, XS))
                                                  , U101(tt()) -> U102(isNaturalKind())
                                                  , U102(tt()) -> U103(isLNatKind())
                                                  , U103(tt()) -> U104(isLNatKind())
                                                  , U104(tt()) -> U105(isNatural())
                                                  , U105(tt()) -> U106(isLNat())
                                                  , U106(tt()) -> tt()
                                                  , U11(tt()) -> U12(isNaturalKind())
                                                  , U111(tt()) -> U112(isLNatKind())
                                                  , U112(tt()) -> tt()
                                                  , U12(tt()) -> U13(isLNat())
                                                  , U121(tt()) -> U122(isLNatKind())
                                                  , U122(tt()) -> tt()
                                                  , U13(tt()) -> U14(isLNatKind())
                                                  , U131(tt()) -> tt()
                                                  , U141(tt()) -> tt()
                                                  , U151(tt()) -> tt()
                                                  , U161(tt()) -> tt()
                                                  , U171(tt()) -> U172(isLNatKind())
                                                  , U172(tt()) -> tt()
                                                  , U181(tt()) -> U182(isLNatKind())
                                                  , U182(tt()) -> U183(isLNat())
                                                  , U183(tt()) -> tt()
                                                  , U191(tt()) -> U192(isNaturalKind())
                                                  , U192(tt()) -> U193(isNatural())
                                                  , U193(tt()) -> tt()
                                                  , U201(tt()) -> U202(isNaturalKind())
                                                  , U202(tt()) -> U203(isLNatKind())
                                                  , U203(tt()) -> U204(isLNatKind())
                                                  , U204(tt()) -> U205(isNatural())
                                                  , U205(tt()) -> U206(isLNat())
                                                  , U206(tt()) -> tt()
                                                  , U21(tt()) -> U22(isLNatKind())
                                                  , U211(tt()) -> tt()
                                                  , U22(tt()) -> U23(isLNat())
                                                  , U221(tt()) -> tt()
                                                  , U23(tt()) -> U24(isLNatKind())
                                                  , U231(tt()) -> U232(isLNatKind())
                                                  , U232(tt()) -> tt()
                                                  , U241(tt()) -> U242(isLNatKind())
                                                  , U242(tt()) -> U243(isLNatKind())
                                                  , U243(tt()) -> U244(isLNatKind())
                                                  , U244(tt()) -> U245(isLNat())
                                                  , U245(tt()) -> U246(isLNat())
                                                  , U246(tt()) -> tt()
                                                  , U251(tt()) -> U252(isNaturalKind())
                                                  , U252(tt()) -> U253(isLNatKind())
                                                  , U253(tt()) -> U254(isLNatKind())
                                                  , U254(tt()) -> U255(isNatural())
                                                  , U255(tt()) -> U256(isLNat())
                                                  , U256(tt()) -> tt()
                                                  , U261(tt()) -> U262(isLNatKind())
                                                  , U262(tt()) -> tt()
                                                  , U271(tt()) -> U272(isLNatKind())
                                                  , U272(tt()) -> tt()
                                                  , U281(tt()) -> U282(isNaturalKind())
                                                  , U291(tt()) -> U292(isNaturalKind())
                                                  , U292(tt()) -> U293(isLNat())
                                                  , U293(tt()) -> U294(isLNatKind())
                                                  , U301(tt()) -> U302(isLNatKind())
                                                  , U302(tt()) -> U303(isLNat())
                                                  , U303(tt()) -> U304(isLNatKind())
                                                  , U31(tt()) -> U32(isNaturalKind())
                                                  , U311(tt()) -> U312(isLNatKind())
                                                  , U32(tt()) -> U33(isLNat())
                                                  , U321(tt()) -> U322(isNaturalKind())
                                                  , U322(tt()) -> U323(isNatural())
                                                  , U323(tt()) -> U324(isNaturalKind())
                                                  , U324(tt()) -> U325(isLNat())
                                                  , U325(tt()) -> U326(isLNatKind())
                                                  , U33(tt()) -> U34(isLNatKind())
                                                  , U331(tt()) -> U332(isNaturalKind())
                                                  , U332(tt()) -> U333(isLNat())
                                                  , U333(tt()) -> U334(isLNatKind())
                                                  , U341(tt()) -> U342(isNaturalKind())
                                                  , U342(tt()) -> U343(isLNat())
                                                  , U343(tt()) -> U344(isLNatKind())
                                                  , U41(tt()) -> U42(isNaturalKind())
                                                  , U42(tt()) -> U43(isLNatKind())
                                                  , U43(tt()) -> U44(isLNatKind())
                                                  , U44(tt()) -> U45(isNatural())
                                                  , U45(tt()) -> U46(isLNat())
                                                  , U46(tt()) -> tt()
                                                  , U51(tt()) -> U52(isNaturalKind())
                                                  , U52(tt()) -> U53(isLNatKind())
                                                  , U53(tt()) -> U54(isLNatKind())
                                                  , U54(tt()) -> U55(isNatural())
                                                  , U55(tt()) -> U56(isLNat())
                                                  , U56(tt()) -> tt()
                                                  , U61(tt()) -> U62(isPLNatKind())
                                                  , U62(tt()) -> U63(isPLNat())
                                                  , U63(tt()) -> tt()
                                                  , U71(tt()) -> U72(isNaturalKind())
                                                  , U72(tt()) -> U73(isNatural())
                                                  , U73(tt()) -> tt()
                                                  , U81(tt()) -> U82(isPLNatKind())
                                                  , U82(tt()) -> U83(isPLNat())
                                                  , U83(tt()) -> tt()
                                                  , U91(tt()) -> U92(isLNatKind())
                                                  , U92(tt()) -> U93(isLNat())
                                                  , U93(tt()) -> tt()
                                                  , afterNth(N, XS) -> U11(isNatural())
                                                  , fst(pair(X, Y)) -> U21(isLNat())
                                                  , head(cons(N)) -> U31(isNatural())
                                                  , isLNat() -> tt()
                                                  , isLNat() -> U41(isNaturalKind())
                                                  , isLNat() -> U51(isNaturalKind())
                                                  , isLNat() -> U61(isPLNatKind())
                                                  , isLNat() -> U71(isNaturalKind())
                                                  , isLNat() -> U81(isPLNatKind())
                                                  , isLNat() -> U91(isLNatKind())
                                                  , isLNat() -> U101(isNaturalKind())
                                                  , isLNatKind() -> tt()
                                                  , isLNatKind() -> U111(isNaturalKind())
                                                  , isLNatKind() -> U121(isNaturalKind())
                                                  , isLNatKind() -> U131(isPLNatKind())
                                                  , isLNatKind() -> U141(isNaturalKind())
                                                  , isLNatKind() -> U151(isPLNatKind())
                                                  , isLNatKind() -> U161(isLNatKind())
                                                  , isLNatKind() -> U171(isNaturalKind())
                                                  , isNatural() -> tt()
                                                  , isNatural() -> U181(isLNatKind())
                                                  , isNatural() -> U191(isNaturalKind())
                                                  , isNatural() -> U201(isNaturalKind())
                                                  , isNaturalKind() -> tt()
                                                  , isNaturalKind() -> U211(isLNatKind())
                                                  , isNaturalKind() -> U221(isNaturalKind())
                                                  , isNaturalKind() -> U231(isNaturalKind())
                                                  , isPLNat() -> U241(isLNatKind())
                                                  , isPLNat() -> U251(isNaturalKind())
                                                  , isPLNatKind() -> U261(isLNatKind())
                                                  , isPLNatKind() -> U271(isNaturalKind())
                                                  , natsFrom(N) -> U281(isNatural())
                                                  , sel(N, XS) -> U291(isNatural())
                                                  , snd(pair(X, Y)) -> U301(isLNat())
                                                  , splitAt(0(), XS) -> U311(isLNat())
                                                  , splitAt(s(N), cons(X)) -> U321(isNatural())
                                                  , tail(cons(N)) -> U331(isNatural())
                                                  , take(N, XS) -> U341(isNatural())}

Try --help.

Tool IRC2

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 LISTUTILITIES complete-noand L

stdout:

MAYBE

The following error(s) occured:

The problem does not contain well-formed TRSs:
   REWRITE relation according to the following TRS
    {  U14(tt()) -> snd(splitAt(N, XS))
     , U24(tt()) -> X
     , U282(tt()) -> cons(N)
     , U294(tt()) -> head(afterNth(N, XS))
     , U304(tt()) -> Y
     , U312(tt()) -> pair(nil(), XS)
     , U326(tt()) -> U327(splitAt(N, XS))
     , U327(pair(YS, ZS)) -> pair(cons(X), ZS)
     , U334(tt()) -> XS
     , U34(tt()) -> N
     , U344(tt()) -> fst(splitAt(N, XS))
     , U101(tt()) -> U102(isNaturalKind())
     , U102(tt()) -> U103(isLNatKind())
     , U103(tt()) -> U104(isLNatKind())
     , U104(tt()) -> U105(isNatural())
     , U105(tt()) -> U106(isLNat())
     , U106(tt()) -> tt()
     , U11(tt()) -> U12(isNaturalKind())
     , U111(tt()) -> U112(isLNatKind())
     , U112(tt()) -> tt()
     , U12(tt()) -> U13(isLNat())
     , U121(tt()) -> U122(isLNatKind())
     , U122(tt()) -> tt()
     , U13(tt()) -> U14(isLNatKind())
     , U131(tt()) -> tt()
     , U141(tt()) -> tt()
     , U151(tt()) -> tt()
     , U161(tt()) -> tt()
     , U171(tt()) -> U172(isLNatKind())
     , U172(tt()) -> tt()
     , U181(tt()) -> U182(isLNatKind())
     , U182(tt()) -> U183(isLNat())
     , U183(tt()) -> tt()
     , U191(tt()) -> U192(isNaturalKind())
     , U192(tt()) -> U193(isNatural())
     , U193(tt()) -> tt()
     , U201(tt()) -> U202(isNaturalKind())
     , U202(tt()) -> U203(isLNatKind())
     , U203(tt()) -> U204(isLNatKind())
     , U204(tt()) -> U205(isNatural())
     , U205(tt()) -> U206(isLNat())
     , U206(tt()) -> tt()
     , U21(tt()) -> U22(isLNatKind())
     , U211(tt()) -> tt()
     , U22(tt()) -> U23(isLNat())
     , U221(tt()) -> tt()
     , U23(tt()) -> U24(isLNatKind())
     , U231(tt()) -> U232(isLNatKind())
     , U232(tt()) -> tt()
     , U241(tt()) -> U242(isLNatKind())
     , U242(tt()) -> U243(isLNatKind())
     , U243(tt()) -> U244(isLNatKind())
     , U244(tt()) -> U245(isLNat())
     , U245(tt()) -> U246(isLNat())
     , U246(tt()) -> tt()
     , U251(tt()) -> U252(isNaturalKind())
     , U252(tt()) -> U253(isLNatKind())
     , U253(tt()) -> U254(isLNatKind())
     , U254(tt()) -> U255(isNatural())
     , U255(tt()) -> U256(isLNat())
     , U256(tt()) -> tt()
     , U261(tt()) -> U262(isLNatKind())
     , U262(tt()) -> tt()
     , U271(tt()) -> U272(isLNatKind())
     , U272(tt()) -> tt()
     , U281(tt()) -> U282(isNaturalKind())
     , U291(tt()) -> U292(isNaturalKind())
     , U292(tt()) -> U293(isLNat())
     , U293(tt()) -> U294(isLNatKind())
     , U301(tt()) -> U302(isLNatKind())
     , U302(tt()) -> U303(isLNat())
     , U303(tt()) -> U304(isLNatKind())
     , U31(tt()) -> U32(isNaturalKind())
     , U311(tt()) -> U312(isLNatKind())
     , U32(tt()) -> U33(isLNat())
     , U321(tt()) -> U322(isNaturalKind())
     , U322(tt()) -> U323(isNatural())
     , U323(tt()) -> U324(isNaturalKind())
     , U324(tt()) -> U325(isLNat())
     , U325(tt()) -> U326(isLNatKind())
     , U33(tt()) -> U34(isLNatKind())
     , U331(tt()) -> U332(isNaturalKind())
     , U332(tt()) -> U333(isLNat())
     , U333(tt()) -> U334(isLNatKind())
     , U341(tt()) -> U342(isNaturalKind())
     , U342(tt()) -> U343(isLNat())
     , U343(tt()) -> U344(isLNatKind())
     , U41(tt()) -> U42(isNaturalKind())
     , U42(tt()) -> U43(isLNatKind())
     , U43(tt()) -> U44(isLNatKind())
     , U44(tt()) -> U45(isNatural())
     , U45(tt()) -> U46(isLNat())
     , U46(tt()) -> tt()
     , U51(tt()) -> U52(isNaturalKind())
     , U52(tt()) -> U53(isLNatKind())
     , U53(tt()) -> U54(isLNatKind())
     , U54(tt()) -> U55(isNatural())
     , U55(tt()) -> U56(isLNat())
     , U56(tt()) -> tt()
     , U61(tt()) -> U62(isPLNatKind())
     , U62(tt()) -> U63(isPLNat())
     , U63(tt()) -> tt()
     , U71(tt()) -> U72(isNaturalKind())
     , U72(tt()) -> U73(isNatural())
     , U73(tt()) -> tt()
     , U81(tt()) -> U82(isPLNatKind())
     , U82(tt()) -> U83(isPLNat())
     , U83(tt()) -> tt()
     , U91(tt()) -> U92(isLNatKind())
     , U92(tt()) -> U93(isLNat())
     , U93(tt()) -> tt()
     , afterNth(N, XS) -> U11(isNatural())
     , fst(pair(X, Y)) -> U21(isLNat())
     , head(cons(N)) -> U31(isNatural())
     , isLNat() -> tt()
     , isLNat() -> U41(isNaturalKind())
     , isLNat() -> U51(isNaturalKind())
     , isLNat() -> U61(isPLNatKind())
     , isLNat() -> U71(isNaturalKind())
     , isLNat() -> U81(isPLNatKind())
     , isLNat() -> U91(isLNatKind())
     , isLNat() -> U101(isNaturalKind())
     , isLNatKind() -> tt()
     , isLNatKind() -> U111(isNaturalKind())
     , isLNatKind() -> U121(isNaturalKind())
     , isLNatKind() -> U131(isPLNatKind())
     , isLNatKind() -> U141(isNaturalKind())
     , isLNatKind() -> U151(isPLNatKind())
     , isLNatKind() -> U161(isLNatKind())
     , isLNatKind() -> U171(isNaturalKind())
     , isNatural() -> tt()
     , isNatural() -> U181(isLNatKind())
     , isNatural() -> U191(isNaturalKind())
     , isNatural() -> U201(isNaturalKind())
     , isNaturalKind() -> tt()
     , isNaturalKind() -> U211(isLNatKind())
     , isNaturalKind() -> U221(isNaturalKind())
     , isNaturalKind() -> U231(isNaturalKind())
     , isPLNat() -> U241(isLNatKind())
     , isPLNat() -> U251(isNaturalKind())
     , isPLNatKind() -> U261(isLNatKind())
     , isPLNatKind() -> U271(isNaturalKind())
     , natsFrom(N) -> U281(isNatural())
     , sel(N, XS) -> U291(isNatural())
     , snd(pair(X, Y)) -> U301(isLNat())
     , splitAt(0(), XS) -> U311(isLNat())
     , splitAt(s(N), cons(X)) -> U321(isNatural())
     , tail(cons(N)) -> U331(isNatural())
     , take(N, XS) -> U341(isNatural())}

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 LISTUTILITIES complete-noand L

stdout:

Tool RC2

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 LISTUTILITIES complete-noand L