Problem Strategy outermost added 08 LISTUTILITIES nokinds-noand L

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputStrategy outermost added 08 LISTUTILITIES nokinds-noand L

stdout:

MAYBE
The following error occured:
 The problem does not contain well-formed TRSs:
                                              
                                                REWRITE relation according to the following TRS
                                                 {  U12(tt()) -> snd(splitAt(N, XS))
                                                  , U161(tt()) -> cons(N)
                                                  , U172(tt()) -> head(afterNth(N, XS))
                                                  , U182(tt()) -> Y
                                                  , U191(tt()) -> pair(nil(), XS)
                                                  , U203(tt()) -> U204(splitAt(N, XS))
                                                  , U204(pair(YS, ZS)) -> pair(cons(X), ZS)
                                                  , U212(tt()) -> XS
                                                  , U22(tt()) -> X
                                                  , U222(tt()) -> fst(splitAt(N, XS))
                                                  , U32(tt()) -> N
                                                  , U101(tt()) -> U102(isLNat())
                                                  , U102(tt()) -> tt()
                                                  , U11(tt()) -> U12(isLNat())
                                                  , U111(tt()) -> tt()
                                                  , U121(tt()) -> tt()
                                                  , U131(tt()) -> U132(isLNat())
                                                  , U132(tt()) -> tt()
                                                  , U141(tt()) -> U142(isLNat())
                                                  , U142(tt()) -> tt()
                                                  , U151(tt()) -> U152(isLNat())
                                                  , U152(tt()) -> tt()
                                                  , U171(tt()) -> U172(isLNat())
                                                  , U181(tt()) -> U182(isLNat())
                                                  , U201(tt()) -> U202(isNatural())
                                                  , U202(tt()) -> U203(isLNat())
                                                  , U21(tt()) -> U22(isLNat())
                                                  , U211(tt()) -> U212(isLNat())
                                                  , U221(tt()) -> U222(isLNat())
                                                  , U31(tt()) -> U32(isLNat())
                                                  , U41(tt()) -> U42(isLNat())
                                                  , U42(tt()) -> tt()
                                                  , U51(tt()) -> U52(isLNat())
                                                  , U52(tt()) -> tt()
                                                  , U61(tt()) -> tt()
                                                  , U71(tt()) -> tt()
                                                  , U81(tt()) -> tt()
                                                  , U91(tt()) -> tt()
                                                  , afterNth(N, XS) -> U11(isNatural())
                                                  , fst(pair(X, Y)) -> U21(isLNat())
                                                  , head(cons(N)) -> U31(isNatural())
                                                  , isLNat() -> tt()
                                                  , isLNat() -> U41(isNatural())
                                                  , isLNat() -> U51(isNatural())
                                                  , isLNat() -> U61(isPLNat())
                                                  , isLNat() -> U71(isNatural())
                                                  , isLNat() -> U81(isPLNat())
                                                  , isLNat() -> U91(isLNat())
                                                  , isLNat() -> U101(isNatural())
                                                  , isNatural() -> tt()
                                                  , isNatural() -> U111(isLNat())
                                                  , isNatural() -> U121(isNatural())
                                                  , isNatural() -> U131(isNatural())
                                                  , isPLNat() -> U141(isLNat())
                                                  , isPLNat() -> U151(isNatural())
                                                  , natsFrom(N) -> U161(isNatural())
                                                  , sel(N, XS) -> U171(isNatural())
                                                  , snd(pair(X, Y)) -> U181(isLNat())
                                                  , splitAt(0(), XS) -> U191(isLNat())
                                                  , splitAt(s(N), cons(X)) -> U201(isNatural())
                                                  , tail(cons(N)) -> U211(isNatural())
                                                  , take(N, XS) -> U221(isNatural())}


Try --help.

Tool IRC2

Execution TimeUnknown
Answer
MAYBE
InputStrategy outermost added 08 LISTUTILITIES nokinds-noand L

stdout:

MAYBE

The following error(s) occured:

 The problem does not contain well-formed TRSs:
   REWRITE relation according to the following TRS and outermost reductions
    {  U12(tt()) -> snd(splitAt(N, XS))
     , U161(tt()) -> cons(N)
     , U172(tt()) -> head(afterNth(N, XS))
     , U182(tt()) -> Y
     , U191(tt()) -> pair(nil(), XS)
     , U203(tt()) -> U204(splitAt(N, XS))
     , U204(pair(YS, ZS)) -> pair(cons(X), ZS)
     , U212(tt()) -> XS
     , U22(tt()) -> X
     , U222(tt()) -> fst(splitAt(N, XS))
     , U32(tt()) -> N
     , U101(tt()) -> U102(isLNat())
     , U102(tt()) -> tt()
     , U11(tt()) -> U12(isLNat())
     , U111(tt()) -> tt()
     , U121(tt()) -> tt()
     , U131(tt()) -> U132(isLNat())
     , U132(tt()) -> tt()
     , U141(tt()) -> U142(isLNat())
     , U142(tt()) -> tt()
     , U151(tt()) -> U152(isLNat())
     , U152(tt()) -> tt()
     , U171(tt()) -> U172(isLNat())
     , U181(tt()) -> U182(isLNat())
     , U201(tt()) -> U202(isNatural())
     , U202(tt()) -> U203(isLNat())
     , U21(tt()) -> U22(isLNat())
     , U211(tt()) -> U212(isLNat())
     , U221(tt()) -> U222(isLNat())
     , U31(tt()) -> U32(isLNat())
     , U41(tt()) -> U42(isLNat())
     , U42(tt()) -> tt()
     , U51(tt()) -> U52(isLNat())
     , U52(tt()) -> tt()
     , U61(tt()) -> tt()
     , U71(tt()) -> tt()
     , U81(tt()) -> tt()
     , U91(tt()) -> tt()
     , afterNth(N, XS) -> U11(isNatural())
     , fst(pair(X, Y)) -> U21(isLNat())
     , head(cons(N)) -> U31(isNatural())
     , isLNat() -> tt()
     , isLNat() -> U41(isNatural())
     , isLNat() -> U51(isNatural())
     , isLNat() -> U61(isPLNat())
     , isLNat() -> U71(isNatural())
     , isLNat() -> U81(isPLNat())
     , isLNat() -> U91(isLNat())
     , isLNat() -> U101(isNatural())
     , isNatural() -> tt()
     , isNatural() -> U111(isLNat())
     , isNatural() -> U121(isNatural())
     , isNatural() -> U131(isNatural())
     , isPLNat() -> U141(isLNat())
     , isPLNat() -> U151(isNatural())
     , natsFrom(N) -> U161(isNatural())
     , sel(N, XS) -> U171(isNatural())
     , snd(pair(X, Y)) -> U181(isLNat())
     , splitAt(0(), XS) -> U191(isLNat())
     , splitAt(s(N), cons(X)) -> U201(isNatural())
     , tail(cons(N)) -> U211(isNatural())
     , take(N, XS) -> U221(isNatural())}

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputStrategy outermost added 08 LISTUTILITIES nokinds-noand L

stdout:

MAYBE
The following error occured:
 The problem does not contain well-formed TRSs:
                                              
                                                REWRITE relation according to the following TRS
                                                 {  U12(tt()) -> snd(splitAt(N, XS))
                                                  , U161(tt()) -> cons(N)
                                                  , U172(tt()) -> head(afterNth(N, XS))
                                                  , U182(tt()) -> Y
                                                  , U191(tt()) -> pair(nil(), XS)
                                                  , U203(tt()) -> U204(splitAt(N, XS))
                                                  , U204(pair(YS, ZS)) -> pair(cons(X), ZS)
                                                  , U212(tt()) -> XS
                                                  , U22(tt()) -> X
                                                  , U222(tt()) -> fst(splitAt(N, XS))
                                                  , U32(tt()) -> N
                                                  , U101(tt()) -> U102(isLNat())
                                                  , U102(tt()) -> tt()
                                                  , U11(tt()) -> U12(isLNat())
                                                  , U111(tt()) -> tt()
                                                  , U121(tt()) -> tt()
                                                  , U131(tt()) -> U132(isLNat())
                                                  , U132(tt()) -> tt()
                                                  , U141(tt()) -> U142(isLNat())
                                                  , U142(tt()) -> tt()
                                                  , U151(tt()) -> U152(isLNat())
                                                  , U152(tt()) -> tt()
                                                  , U171(tt()) -> U172(isLNat())
                                                  , U181(tt()) -> U182(isLNat())
                                                  , U201(tt()) -> U202(isNatural())
                                                  , U202(tt()) -> U203(isLNat())
                                                  , U21(tt()) -> U22(isLNat())
                                                  , U211(tt()) -> U212(isLNat())
                                                  , U221(tt()) -> U222(isLNat())
                                                  , U31(tt()) -> U32(isLNat())
                                                  , U41(tt()) -> U42(isLNat())
                                                  , U42(tt()) -> tt()
                                                  , U51(tt()) -> U52(isLNat())
                                                  , U52(tt()) -> tt()
                                                  , U61(tt()) -> tt()
                                                  , U71(tt()) -> tt()
                                                  , U81(tt()) -> tt()
                                                  , U91(tt()) -> tt()
                                                  , afterNth(N, XS) -> U11(isNatural())
                                                  , fst(pair(X, Y)) -> U21(isLNat())
                                                  , head(cons(N)) -> U31(isNatural())
                                                  , isLNat() -> tt()
                                                  , isLNat() -> U41(isNatural())
                                                  , isLNat() -> U51(isNatural())
                                                  , isLNat() -> U61(isPLNat())
                                                  , isLNat() -> U71(isNatural())
                                                  , isLNat() -> U81(isPLNat())
                                                  , isLNat() -> U91(isLNat())
                                                  , isLNat() -> U101(isNatural())
                                                  , isNatural() -> tt()
                                                  , isNatural() -> U111(isLNat())
                                                  , isNatural() -> U121(isNatural())
                                                  , isNatural() -> U131(isNatural())
                                                  , isPLNat() -> U141(isLNat())
                                                  , isPLNat() -> U151(isNatural())
                                                  , natsFrom(N) -> U161(isNatural())
                                                  , sel(N, XS) -> U171(isNatural())
                                                  , snd(pair(X, Y)) -> U181(isLNat())
                                                  , splitAt(0(), XS) -> U191(isLNat())
                                                  , splitAt(s(N), cons(X)) -> U201(isNatural())
                                                  , tail(cons(N)) -> U211(isNatural())
                                                  , take(N, XS) -> U221(isNatural())}


Try --help.

Tool RC2

Execution TimeUnknown
Answer
MAYBE
InputStrategy outermost added 08 LISTUTILITIES nokinds-noand L

stdout:

MAYBE

The following error(s) occured:

 The problem does not contain well-formed TRSs:
   REWRITE relation according to the following TRS and outermost reductions
    {  U12(tt()) -> snd(splitAt(N, XS))
     , U161(tt()) -> cons(N)
     , U172(tt()) -> head(afterNth(N, XS))
     , U182(tt()) -> Y
     , U191(tt()) -> pair(nil(), XS)
     , U203(tt()) -> U204(splitAt(N, XS))
     , U204(pair(YS, ZS)) -> pair(cons(X), ZS)
     , U212(tt()) -> XS
     , U22(tt()) -> X
     , U222(tt()) -> fst(splitAt(N, XS))
     , U32(tt()) -> N
     , U101(tt()) -> U102(isLNat())
     , U102(tt()) -> tt()
     , U11(tt()) -> U12(isLNat())
     , U111(tt()) -> tt()
     , U121(tt()) -> tt()
     , U131(tt()) -> U132(isLNat())
     , U132(tt()) -> tt()
     , U141(tt()) -> U142(isLNat())
     , U142(tt()) -> tt()
     , U151(tt()) -> U152(isLNat())
     , U152(tt()) -> tt()
     , U171(tt()) -> U172(isLNat())
     , U181(tt()) -> U182(isLNat())
     , U201(tt()) -> U202(isNatural())
     , U202(tt()) -> U203(isLNat())
     , U21(tt()) -> U22(isLNat())
     , U211(tt()) -> U212(isLNat())
     , U221(tt()) -> U222(isLNat())
     , U31(tt()) -> U32(isLNat())
     , U41(tt()) -> U42(isLNat())
     , U42(tt()) -> tt()
     , U51(tt()) -> U52(isLNat())
     , U52(tt()) -> tt()
     , U61(tt()) -> tt()
     , U71(tt()) -> tt()
     , U81(tt()) -> tt()
     , U91(tt()) -> tt()
     , afterNth(N, XS) -> U11(isNatural())
     , fst(pair(X, Y)) -> U21(isLNat())
     , head(cons(N)) -> U31(isNatural())
     , isLNat() -> tt()
     , isLNat() -> U41(isNatural())
     , isLNat() -> U51(isNatural())
     , isLNat() -> U61(isPLNat())
     , isLNat() -> U71(isNatural())
     , isLNat() -> U81(isPLNat())
     , isLNat() -> U91(isLNat())
     , isLNat() -> U101(isNatural())
     , isNatural() -> tt()
     , isNatural() -> U111(isLNat())
     , isNatural() -> U121(isNatural())
     , isNatural() -> U131(isNatural())
     , isPLNat() -> U141(isLNat())
     , isPLNat() -> U151(isNatural())
     , natsFrom(N) -> U161(isNatural())
     , sel(N, XS) -> U171(isNatural())
     , snd(pair(X, Y)) -> U181(isLNat())
     , splitAt(0(), XS) -> U191(isLNat())
     , splitAt(s(N), cons(X)) -> U201(isNatural())
     , tail(cons(N)) -> U211(isNatural())
     , take(N, XS) -> U221(isNatural())}