Problem Transformed CSR 04 LISTUTILITIES complete L

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputTransformed CSR 04 LISTUTILITIES complete L

stdout:

MAYBE
The following error occured:
 The problem does not contain well-formed TRSs:
                                              
                                                REWRITE relation according to the following TRS
                                                 {  U11(tt()) -> snd(splitAt(N, XS))
                                                  , U161(tt()) -> cons(N)
                                                  , U171(tt()) -> head(afterNth(N, XS))
                                                  , U181(tt()) -> Y
                                                  , U191(tt()) -> pair(nil(), XS)
                                                  , U201(tt()) -> U202(splitAt(N, XS))
                                                  , U202(pair(YS, ZS)) -> pair(cons(X), ZS)
                                                  , U21(tt()) -> X
                                                  , U211(tt()) -> XS
                                                  , U221(tt()) -> fst(splitAt(N, XS))
                                                  , U31(tt()) -> N
                                                  , and(tt()) -> X
                                                  , U101(tt()) -> U102(isNatural())
                                                  , U102(tt()) -> U103(isLNat())
                                                  , U103(tt()) -> tt()
                                                  , U111(tt()) -> U112(isLNat())
                                                  , U112(tt()) -> tt()
                                                  , U121(tt()) -> U122(isNatural())
                                                  , U122(tt()) -> tt()
                                                  , U131(tt()) -> U132(isNatural())
                                                  , U132(tt()) -> U133(isLNat())
                                                  , U133(tt()) -> tt()
                                                  , U141(tt()) -> U142(isLNat())
                                                  , U142(tt()) -> U143(isLNat())
                                                  , U143(tt()) -> tt()
                                                  , U151(tt()) -> U152(isNatural())
                                                  , U152(tt()) -> U153(isLNat())
                                                  , U153(tt()) -> tt()
                                                  , U41(tt()) -> U42(isNatural())
                                                  , U42(tt()) -> U43(isLNat())
                                                  , U43(tt()) -> tt()
                                                  , U51(tt()) -> U52(isNatural())
                                                  , U52(tt()) -> U53(isLNat())
                                                  , U53(tt()) -> tt()
                                                  , U61(tt()) -> U62(isPLNat())
                                                  , U62(tt()) -> tt()
                                                  , U71(tt()) -> U72(isNatural())
                                                  , U72(tt()) -> tt()
                                                  , U81(tt()) -> U82(isPLNat())
                                                  , U82(tt()) -> tt()
                                                  , U91(tt()) -> U92(isLNat())
                                                  , U92(tt()) -> tt()
                                                  , afterNth(N, XS) -> U11(and(and(isNatural())))
                                                  , fst(pair(X, Y)) -> U21(and(and(isLNat())))
                                                  , head(cons(N)) -> U31(and(and(isNatural())))
                                                  , isLNat() -> tt()
                                                  , isLNat() -> U41(and(isNaturalKind()))
                                                  , isLNat() -> U51(and(isNaturalKind()))
                                                  , isLNat() -> U61(isPLNatKind())
                                                  , isLNat() -> U71(isNaturalKind())
                                                  , isLNat() -> U81(isPLNatKind())
                                                  , isLNat() -> U91(isLNatKind())
                                                  , isLNat() -> U101(and(isNaturalKind()))
                                                  , isLNatKind() -> tt()
                                                  , isLNatKind() -> and(isNaturalKind())
                                                  , isLNatKind() -> isPLNatKind()
                                                  , isLNatKind() -> isNaturalKind()
                                                  , isLNatKind() -> isLNatKind()
                                                  , isNatural() -> tt()
                                                  , isNatural() -> U111(isLNatKind())
                                                  , isNatural() -> U121(isNaturalKind())
                                                  , isNatural() -> U131(and(isNaturalKind()))
                                                  , isNaturalKind() -> tt()
                                                  , isNaturalKind() -> isLNatKind()
                                                  , isNaturalKind() -> isNaturalKind()
                                                  , isNaturalKind() -> and(isNaturalKind())
                                                  , isPLNat() -> U141(and(isLNatKind()))
                                                  , isPLNat() -> U151(and(isNaturalKind()))
                                                  , isPLNatKind() -> and(isLNatKind())
                                                  , isPLNatKind() -> and(isNaturalKind())
                                                  , natsFrom(N) -> U161(and(isNatural()))
                                                  , sel(N, XS) -> U171(and(and(isNatural())))
                                                  , snd(pair(X, Y)) -> U181(and(and(isLNat())))
                                                  , splitAt(0(), XS) -> U191(and(isLNat()))
                                                  , splitAt(s(N), cons(X)) ->
                                                    U201(and(and(isNatural())))
                                                  , tail(cons(N)) -> U211(and(and(isNatural())))
                                                  , take(N, XS) -> U221(and(and(isNatural())))}


Try --help.

Tool IRC2

Execution TimeUnknown
Answer
MAYBE
InputTransformed CSR 04 LISTUTILITIES complete L

stdout:

MAYBE

The following error(s) occured:

 The problem does not contain well-formed TRSs:
   REWRITE relation according to the following TRS
    {  U11(tt()) -> snd(splitAt(N, XS))
     , U161(tt()) -> cons(N)
     , U171(tt()) -> head(afterNth(N, XS))
     , U181(tt()) -> Y
     , U191(tt()) -> pair(nil(), XS)
     , U201(tt()) -> U202(splitAt(N, XS))
     , U202(pair(YS, ZS)) -> pair(cons(X), ZS)
     , U21(tt()) -> X
     , U211(tt()) -> XS
     , U221(tt()) -> fst(splitAt(N, XS))
     , U31(tt()) -> N
     , and(tt()) -> X
     , U101(tt()) -> U102(isNatural())
     , U102(tt()) -> U103(isLNat())
     , U103(tt()) -> tt()
     , U111(tt()) -> U112(isLNat())
     , U112(tt()) -> tt()
     , U121(tt()) -> U122(isNatural())
     , U122(tt()) -> tt()
     , U131(tt()) -> U132(isNatural())
     , U132(tt()) -> U133(isLNat())
     , U133(tt()) -> tt()
     , U141(tt()) -> U142(isLNat())
     , U142(tt()) -> U143(isLNat())
     , U143(tt()) -> tt()
     , U151(tt()) -> U152(isNatural())
     , U152(tt()) -> U153(isLNat())
     , U153(tt()) -> tt()
     , U41(tt()) -> U42(isNatural())
     , U42(tt()) -> U43(isLNat())
     , U43(tt()) -> tt()
     , U51(tt()) -> U52(isNatural())
     , U52(tt()) -> U53(isLNat())
     , U53(tt()) -> tt()
     , U61(tt()) -> U62(isPLNat())
     , U62(tt()) -> tt()
     , U71(tt()) -> U72(isNatural())
     , U72(tt()) -> tt()
     , U81(tt()) -> U82(isPLNat())
     , U82(tt()) -> tt()
     , U91(tt()) -> U92(isLNat())
     , U92(tt()) -> tt()
     , afterNth(N, XS) -> U11(and(and(isNatural())))
     , fst(pair(X, Y)) -> U21(and(and(isLNat())))
     , head(cons(N)) -> U31(and(and(isNatural())))
     , isLNat() -> tt()
     , isLNat() -> U41(and(isNaturalKind()))
     , isLNat() -> U51(and(isNaturalKind()))
     , isLNat() -> U61(isPLNatKind())
     , isLNat() -> U71(isNaturalKind())
     , isLNat() -> U81(isPLNatKind())
     , isLNat() -> U91(isLNatKind())
     , isLNat() -> U101(and(isNaturalKind()))
     , isLNatKind() -> tt()
     , isLNatKind() -> and(isNaturalKind())
     , isLNatKind() -> isPLNatKind()
     , isLNatKind() -> isNaturalKind()
     , isLNatKind() -> isLNatKind()
     , isNatural() -> tt()
     , isNatural() -> U111(isLNatKind())
     , isNatural() -> U121(isNaturalKind())
     , isNatural() -> U131(and(isNaturalKind()))
     , isNaturalKind() -> tt()
     , isNaturalKind() -> isLNatKind()
     , isNaturalKind() -> isNaturalKind()
     , isNaturalKind() -> and(isNaturalKind())
     , isPLNat() -> U141(and(isLNatKind()))
     , isPLNat() -> U151(and(isNaturalKind()))
     , isPLNatKind() -> and(isLNatKind())
     , isPLNatKind() -> and(isNaturalKind())
     , natsFrom(N) -> U161(and(isNatural()))
     , sel(N, XS) -> U171(and(and(isNatural())))
     , snd(pair(X, Y)) -> U181(and(and(isLNat())))
     , splitAt(0(), XS) -> U191(and(isLNat()))
     , splitAt(s(N), cons(X)) -> U201(and(and(isNatural())))
     , tail(cons(N)) -> U211(and(and(isNatural())))
     , take(N, XS) -> U221(and(and(isNatural())))}

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputTransformed CSR 04 LISTUTILITIES complete L

stdout:

MAYBE
The following error occured:
 The problem does not contain well-formed TRSs:
                                              
                                                REWRITE relation according to the following TRS
                                                 {  U11(tt()) -> snd(splitAt(N, XS))
                                                  , U161(tt()) -> cons(N)
                                                  , U171(tt()) -> head(afterNth(N, XS))
                                                  , U181(tt()) -> Y
                                                  , U191(tt()) -> pair(nil(), XS)
                                                  , U201(tt()) -> U202(splitAt(N, XS))
                                                  , U202(pair(YS, ZS)) -> pair(cons(X), ZS)
                                                  , U21(tt()) -> X
                                                  , U211(tt()) -> XS
                                                  , U221(tt()) -> fst(splitAt(N, XS))
                                                  , U31(tt()) -> N
                                                  , and(tt()) -> X
                                                  , U101(tt()) -> U102(isNatural())
                                                  , U102(tt()) -> U103(isLNat())
                                                  , U103(tt()) -> tt()
                                                  , U111(tt()) -> U112(isLNat())
                                                  , U112(tt()) -> tt()
                                                  , U121(tt()) -> U122(isNatural())
                                                  , U122(tt()) -> tt()
                                                  , U131(tt()) -> U132(isNatural())
                                                  , U132(tt()) -> U133(isLNat())
                                                  , U133(tt()) -> tt()
                                                  , U141(tt()) -> U142(isLNat())
                                                  , U142(tt()) -> U143(isLNat())
                                                  , U143(tt()) -> tt()
                                                  , U151(tt()) -> U152(isNatural())
                                                  , U152(tt()) -> U153(isLNat())
                                                  , U153(tt()) -> tt()
                                                  , U41(tt()) -> U42(isNatural())
                                                  , U42(tt()) -> U43(isLNat())
                                                  , U43(tt()) -> tt()
                                                  , U51(tt()) -> U52(isNatural())
                                                  , U52(tt()) -> U53(isLNat())
                                                  , U53(tt()) -> tt()
                                                  , U61(tt()) -> U62(isPLNat())
                                                  , U62(tt()) -> tt()
                                                  , U71(tt()) -> U72(isNatural())
                                                  , U72(tt()) -> tt()
                                                  , U81(tt()) -> U82(isPLNat())
                                                  , U82(tt()) -> tt()
                                                  , U91(tt()) -> U92(isLNat())
                                                  , U92(tt()) -> tt()
                                                  , afterNth(N, XS) -> U11(and(and(isNatural())))
                                                  , fst(pair(X, Y)) -> U21(and(and(isLNat())))
                                                  , head(cons(N)) -> U31(and(and(isNatural())))
                                                  , isLNat() -> tt()
                                                  , isLNat() -> U41(and(isNaturalKind()))
                                                  , isLNat() -> U51(and(isNaturalKind()))
                                                  , isLNat() -> U61(isPLNatKind())
                                                  , isLNat() -> U71(isNaturalKind())
                                                  , isLNat() -> U81(isPLNatKind())
                                                  , isLNat() -> U91(isLNatKind())
                                                  , isLNat() -> U101(and(isNaturalKind()))
                                                  , isLNatKind() -> tt()
                                                  , isLNatKind() -> and(isNaturalKind())
                                                  , isLNatKind() -> isPLNatKind()
                                                  , isLNatKind() -> isNaturalKind()
                                                  , isLNatKind() -> isLNatKind()
                                                  , isNatural() -> tt()
                                                  , isNatural() -> U111(isLNatKind())
                                                  , isNatural() -> U121(isNaturalKind())
                                                  , isNatural() -> U131(and(isNaturalKind()))
                                                  , isNaturalKind() -> tt()
                                                  , isNaturalKind() -> isLNatKind()
                                                  , isNaturalKind() -> isNaturalKind()
                                                  , isNaturalKind() -> and(isNaturalKind())
                                                  , isPLNat() -> U141(and(isLNatKind()))
                                                  , isPLNat() -> U151(and(isNaturalKind()))
                                                  , isPLNatKind() -> and(isLNatKind())
                                                  , isPLNatKind() -> and(isNaturalKind())
                                                  , natsFrom(N) -> U161(and(isNatural()))
                                                  , sel(N, XS) -> U171(and(and(isNatural())))
                                                  , snd(pair(X, Y)) -> U181(and(and(isLNat())))
                                                  , splitAt(0(), XS) -> U191(and(isLNat()))
                                                  , splitAt(s(N), cons(X)) ->
                                                    U201(and(and(isNatural())))
                                                  , tail(cons(N)) -> U211(and(and(isNatural())))
                                                  , take(N, XS) -> U221(and(and(isNatural())))}


Try --help.

Tool RC2

Execution TimeUnknown
Answer
MAYBE
InputTransformed CSR 04 LISTUTILITIES complete L

stdout:

MAYBE

The following error(s) occured:

 The problem does not contain well-formed TRSs:
   REWRITE relation according to the following TRS
    {  U11(tt()) -> snd(splitAt(N, XS))
     , U161(tt()) -> cons(N)
     , U171(tt()) -> head(afterNth(N, XS))
     , U181(tt()) -> Y
     , U191(tt()) -> pair(nil(), XS)
     , U201(tt()) -> U202(splitAt(N, XS))
     , U202(pair(YS, ZS)) -> pair(cons(X), ZS)
     , U21(tt()) -> X
     , U211(tt()) -> XS
     , U221(tt()) -> fst(splitAt(N, XS))
     , U31(tt()) -> N
     , and(tt()) -> X
     , U101(tt()) -> U102(isNatural())
     , U102(tt()) -> U103(isLNat())
     , U103(tt()) -> tt()
     , U111(tt()) -> U112(isLNat())
     , U112(tt()) -> tt()
     , U121(tt()) -> U122(isNatural())
     , U122(tt()) -> tt()
     , U131(tt()) -> U132(isNatural())
     , U132(tt()) -> U133(isLNat())
     , U133(tt()) -> tt()
     , U141(tt()) -> U142(isLNat())
     , U142(tt()) -> U143(isLNat())
     , U143(tt()) -> tt()
     , U151(tt()) -> U152(isNatural())
     , U152(tt()) -> U153(isLNat())
     , U153(tt()) -> tt()
     , U41(tt()) -> U42(isNatural())
     , U42(tt()) -> U43(isLNat())
     , U43(tt()) -> tt()
     , U51(tt()) -> U52(isNatural())
     , U52(tt()) -> U53(isLNat())
     , U53(tt()) -> tt()
     , U61(tt()) -> U62(isPLNat())
     , U62(tt()) -> tt()
     , U71(tt()) -> U72(isNatural())
     , U72(tt()) -> tt()
     , U81(tt()) -> U82(isPLNat())
     , U82(tt()) -> tt()
     , U91(tt()) -> U92(isLNat())
     , U92(tt()) -> tt()
     , afterNth(N, XS) -> U11(and(and(isNatural())))
     , fst(pair(X, Y)) -> U21(and(and(isLNat())))
     , head(cons(N)) -> U31(and(and(isNatural())))
     , isLNat() -> tt()
     , isLNat() -> U41(and(isNaturalKind()))
     , isLNat() -> U51(and(isNaturalKind()))
     , isLNat() -> U61(isPLNatKind())
     , isLNat() -> U71(isNaturalKind())
     , isLNat() -> U81(isPLNatKind())
     , isLNat() -> U91(isLNatKind())
     , isLNat() -> U101(and(isNaturalKind()))
     , isLNatKind() -> tt()
     , isLNatKind() -> and(isNaturalKind())
     , isLNatKind() -> isPLNatKind()
     , isLNatKind() -> isNaturalKind()
     , isLNatKind() -> isLNatKind()
     , isNatural() -> tt()
     , isNatural() -> U111(isLNatKind())
     , isNatural() -> U121(isNaturalKind())
     , isNatural() -> U131(and(isNaturalKind()))
     , isNaturalKind() -> tt()
     , isNaturalKind() -> isLNatKind()
     , isNaturalKind() -> isNaturalKind()
     , isNaturalKind() -> and(isNaturalKind())
     , isPLNat() -> U141(and(isLNatKind()))
     , isPLNat() -> U151(and(isNaturalKind()))
     , isPLNatKind() -> and(isLNatKind())
     , isPLNatKind() -> and(isNaturalKind())
     , natsFrom(N) -> U161(and(isNatural()))
     , sel(N, XS) -> U171(and(and(isNatural())))
     , snd(pair(X, Y)) -> U181(and(and(isLNat())))
     , splitAt(0(), XS) -> U191(and(isLNat()))
     , splitAt(s(N), cons(X)) -> U201(and(and(isNatural())))
     , tail(cons(N)) -> U211(and(and(isNatural())))
     , take(N, XS) -> U221(and(and(isNatural())))}