MAYBE 1178.47/299.88 MAYBE 1178.47/299.88 1178.47/299.88 We are left with following problem, upon which TcT provides the 1178.47/299.88 certificate MAYBE. 1178.47/299.88 1178.47/299.88 Strict Trs: 1178.47/299.88 { a__U101(X1, X2, X3) -> U101(X1, X2, X3) 1178.47/299.88 , a__U101(tt(), N, XS) -> a__fst(a__splitAt(mark(N), mark(XS))) 1178.47/299.88 , a__fst(X) -> fst(X) 1178.47/299.88 , a__fst(pair(X, Y)) -> a__U21(a__and(a__isLNat(X), isLNat(Y)), X) 1178.47/299.88 , a__splitAt(X1, X2) -> splitAt(X1, X2) 1178.47/299.88 , a__splitAt(s(N), cons(X, XS)) -> 1178.47/299.88 a__U81(a__and(a__isNatural(N), and(isNatural(X), isLNat(XS))), 1178.47/299.88 N, 1178.47/299.88 X, 1178.47/299.88 XS) 1178.47/299.88 , a__splitAt(0(), XS) -> a__U71(a__isLNat(XS), XS) 1178.47/299.88 , mark(tt()) -> tt() 1178.47/299.88 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 1178.47/299.88 , mark(natsFrom(X)) -> a__natsFrom(mark(X)) 1178.47/299.88 , mark(s(X)) -> s(mark(X)) 1178.47/299.88 , mark(pair(X1, X2)) -> pair(mark(X1), mark(X2)) 1178.47/299.88 , mark(nil()) -> nil() 1178.47/299.88 , mark(isLNat(X)) -> a__isLNat(X) 1178.47/299.88 , mark(afterNth(X1, X2)) -> a__afterNth(mark(X1), mark(X2)) 1178.47/299.88 , mark(fst(X)) -> a__fst(mark(X)) 1178.47/299.88 , mark(snd(X)) -> a__snd(mark(X)) 1178.47/299.88 , mark(tail(X)) -> a__tail(mark(X)) 1178.47/299.88 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 1178.47/299.88 , mark(0()) -> 0() 1178.47/299.88 , mark(head(X)) -> a__head(mark(X)) 1178.47/299.88 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1178.47/299.88 , mark(splitAt(X1, X2)) -> a__splitAt(mark(X1), mark(X2)) 1178.47/299.88 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1178.47/299.88 , mark(isNatural(X)) -> a__isNatural(X) 1178.47/299.88 , mark(U101(X1, X2, X3)) -> a__U101(mark(X1), X2, X3) 1178.47/299.88 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 1178.47/299.88 , mark(U21(X1, X2)) -> a__U21(mark(X1), X2) 1178.47/299.88 , mark(U31(X1, X2)) -> a__U31(mark(X1), X2) 1178.47/299.88 , mark(U41(X1, X2)) -> a__U41(mark(X1), X2) 1178.47/299.88 , mark(U51(X1, X2, X3)) -> a__U51(mark(X1), X2, X3) 1178.47/299.88 , mark(U61(X1, X2)) -> a__U61(mark(X1), X2) 1178.47/299.88 , mark(U71(X1, X2)) -> a__U71(mark(X1), X2) 1178.47/299.88 , mark(U81(X1, X2, X3, X4)) -> a__U81(mark(X1), X2, X3, X4) 1178.47/299.88 , mark(U82(X1, X2)) -> a__U82(mark(X1), X2) 1178.47/299.88 , mark(U91(X1, X2)) -> a__U91(mark(X1), X2) 1178.47/299.88 , mark(isPLNat(X)) -> a__isPLNat(X) 1178.47/299.88 , a__U11(X1, X2, X3) -> U11(X1, X2, X3) 1178.47/299.88 , a__U11(tt(), N, XS) -> a__snd(a__splitAt(mark(N), mark(XS))) 1178.47/299.88 , a__snd(X) -> snd(X) 1178.47/299.88 , a__snd(pair(X, Y)) -> a__U61(a__and(a__isLNat(X), isLNat(Y)), Y) 1178.47/299.88 , a__U21(X1, X2) -> U21(X1, X2) 1178.47/299.88 , a__U21(tt(), X) -> mark(X) 1178.47/299.88 , a__U31(X1, X2) -> U31(X1, X2) 1178.47/299.88 , a__U31(tt(), N) -> mark(N) 1178.47/299.88 , a__U41(X1, X2) -> U41(X1, X2) 1178.47/299.88 , a__U41(tt(), N) -> cons(mark(N), natsFrom(s(N))) 1178.47/299.88 , a__U51(X1, X2, X3) -> U51(X1, X2, X3) 1178.47/299.88 , a__U51(tt(), N, XS) -> a__head(a__afterNth(mark(N), mark(XS))) 1178.47/299.88 , a__head(X) -> head(X) 1178.47/299.88 , a__head(cons(N, XS)) -> 1178.47/299.88 a__U31(a__and(a__isNatural(N), isLNat(XS)), N) 1178.47/299.88 , a__afterNth(N, XS) -> 1178.47/299.88 a__U11(a__and(a__isNatural(N), isLNat(XS)), N, XS) 1178.47/299.88 , a__afterNth(X1, X2) -> afterNth(X1, X2) 1178.47/299.88 , a__U61(X1, X2) -> U61(X1, X2) 1178.47/299.88 , a__U61(tt(), Y) -> mark(Y) 1178.47/299.88 , a__U71(X1, X2) -> U71(X1, X2) 1178.47/299.88 , a__U71(tt(), XS) -> pair(nil(), mark(XS)) 1178.47/299.88 , a__U81(X1, X2, X3, X4) -> U81(X1, X2, X3, X4) 1178.47/299.88 , a__U81(tt(), N, X, XS) -> 1178.47/299.88 a__U82(a__splitAt(mark(N), mark(XS)), X) 1178.47/299.88 , a__U82(X1, X2) -> U82(X1, X2) 1178.47/299.88 , a__U82(pair(YS, ZS), X) -> pair(cons(mark(X), YS), mark(ZS)) 1178.47/299.88 , a__U91(X1, X2) -> U91(X1, X2) 1178.47/299.88 , a__U91(tt(), XS) -> mark(XS) 1178.47/299.88 , a__and(X1, X2) -> and(X1, X2) 1178.47/299.88 , a__and(tt(), X) -> mark(X) 1178.47/299.88 , a__isNatural(X) -> isNatural(X) 1178.47/299.88 , a__isNatural(s(V1)) -> a__isNatural(V1) 1178.47/299.88 , a__isNatural(0()) -> tt() 1178.47/299.88 , a__isNatural(head(V1)) -> a__isLNat(V1) 1178.47/299.88 , a__isNatural(sel(V1, V2)) -> a__and(a__isNatural(V1), isLNat(V2)) 1178.47/299.88 , a__isLNat(X) -> isLNat(X) 1178.47/299.88 , a__isLNat(cons(V1, V2)) -> a__and(a__isNatural(V1), isLNat(V2)) 1178.47/299.88 , a__isLNat(natsFrom(V1)) -> a__isNatural(V1) 1178.47/299.88 , a__isLNat(nil()) -> tt() 1178.47/299.88 , a__isLNat(afterNth(V1, V2)) -> 1178.47/299.88 a__and(a__isNatural(V1), isLNat(V2)) 1178.47/299.88 , a__isLNat(fst(V1)) -> a__isPLNat(V1) 1178.47/299.88 , a__isLNat(snd(V1)) -> a__isPLNat(V1) 1178.47/299.88 , a__isLNat(tail(V1)) -> a__isLNat(V1) 1178.47/299.88 , a__isLNat(take(V1, V2)) -> a__and(a__isNatural(V1), isLNat(V2)) 1178.47/299.88 , a__isPLNat(X) -> isPLNat(X) 1178.47/299.88 , a__isPLNat(pair(V1, V2)) -> a__and(a__isLNat(V1), isLNat(V2)) 1178.47/299.88 , a__isPLNat(splitAt(V1, V2)) -> 1178.47/299.88 a__and(a__isNatural(V1), isLNat(V2)) 1178.47/299.88 , a__natsFrom(N) -> a__U41(a__isNatural(N), N) 1178.47/299.88 , a__natsFrom(X) -> natsFrom(X) 1178.47/299.88 , a__sel(N, XS) -> 1178.47/299.88 a__U51(a__and(a__isNatural(N), isLNat(XS)), N, XS) 1178.47/299.88 , a__sel(X1, X2) -> sel(X1, X2) 1178.47/299.88 , a__tail(X) -> tail(X) 1178.47/299.88 , a__tail(cons(N, XS)) -> 1178.47/299.88 a__U91(a__and(a__isNatural(N), isLNat(XS)), XS) 1178.47/299.88 , a__take(N, XS) -> 1178.47/299.88 a__U101(a__and(a__isNatural(N), isLNat(XS)), N, XS) 1178.47/299.88 , a__take(X1, X2) -> take(X1, X2) } 1178.47/299.88 Obligation: 1178.47/299.88 runtime complexity 1178.47/299.88 Answer: 1178.47/299.88 MAYBE 1178.47/299.88 1178.47/299.88 None of the processors succeeded. 1178.47/299.88 1178.47/299.88 Details of failed attempt(s): 1178.47/299.88 ----------------------------- 1178.47/299.88 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1178.47/299.88 following reason: 1178.47/299.88 1178.47/299.88 Computation stopped due to timeout after 297.0 seconds. 1178.47/299.88 1178.47/299.88 2) 'Best' failed due to the following reason: 1178.47/299.88 1178.47/299.88 None of the processors succeeded. 1178.47/299.88 1178.47/299.88 Details of failed attempt(s): 1178.47/299.88 ----------------------------- 1178.47/299.88 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1178.47/299.88 seconds)' failed due to the following reason: 1178.47/299.88 1178.47/299.88 Computation stopped due to timeout after 148.0 seconds. 1178.47/299.88 1178.47/299.88 2) 'Best' failed due to the following reason: 1178.47/299.88 1178.47/299.88 None of the processors succeeded. 1178.47/299.88 1178.47/299.88 Details of failed attempt(s): 1178.47/299.88 ----------------------------- 1178.47/299.88 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1178.47/299.88 following reason: 1178.47/299.88 1178.47/299.88 The processor is inapplicable, reason: 1178.47/299.88 Processor only applicable for innermost runtime complexity analysis 1178.47/299.88 1178.47/299.88 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1178.47/299.88 to the following reason: 1178.47/299.88 1178.47/299.88 The processor is inapplicable, reason: 1178.47/299.88 Processor only applicable for innermost runtime complexity analysis 1178.47/299.88 1178.47/299.88 1178.47/299.88 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1178.47/299.88 failed due to the following reason: 1178.47/299.88 1178.47/299.88 None of the processors succeeded. 1178.47/299.88 1178.47/299.88 Details of failed attempt(s): 1178.47/299.88 ----------------------------- 1178.47/299.88 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1178.47/299.88 failed due to the following reason: 1178.47/299.88 1178.47/299.88 match-boundness of the problem could not be verified. 1178.47/299.88 1178.47/299.88 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1178.47/299.88 failed due to the following reason: 1178.47/299.88 1178.47/299.88 match-boundness of the problem could not be verified. 1178.47/299.88 1178.47/299.88 1178.47/299.88 1178.47/299.88 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1178.47/299.88 the following reason: 1178.47/299.88 1178.47/299.88 We add the following weak dependency pairs: 1178.47/299.88 1178.47/299.88 Strict DPs: 1178.47/299.88 { a__U101^#(X1, X2, X3) -> c_1(X1, X2, X3) 1178.47/299.88 , a__U101^#(tt(), N, XS) -> 1178.47/299.88 c_2(a__fst^#(a__splitAt(mark(N), mark(XS)))) 1178.47/299.88 , a__fst^#(X) -> c_3(X) 1178.47/299.88 , a__fst^#(pair(X, Y)) -> 1178.47/299.88 c_4(a__U21^#(a__and(a__isLNat(X), isLNat(Y)), X)) 1178.47/299.88 , a__U21^#(X1, X2) -> c_42(X1, X2) 1178.47/299.88 , a__U21^#(tt(), X) -> c_43(mark^#(X)) 1178.47/299.88 , a__splitAt^#(X1, X2) -> c_5(X1, X2) 1178.47/299.88 , a__splitAt^#(s(N), cons(X, XS)) -> 1178.47/299.88 c_6(a__U81^#(a__and(a__isNatural(N), 1178.47/299.88 and(isNatural(X), isLNat(XS))), 1178.47/299.88 N, 1178.47/299.88 X, 1178.47/299.88 XS)) 1178.47/299.88 , a__splitAt^#(0(), XS) -> c_7(a__U71^#(a__isLNat(XS), XS)) 1178.47/299.88 , a__U81^#(X1, X2, X3, X4) -> c_58(X1, X2, X3, X4) 1178.47/299.88 , a__U81^#(tt(), N, X, XS) -> 1178.47/299.88 c_59(a__U82^#(a__splitAt(mark(N), mark(XS)), X)) 1178.47/299.88 , a__U71^#(X1, X2) -> c_56(X1, X2) 1178.47/299.88 , a__U71^#(tt(), XS) -> c_57(mark^#(XS)) 1178.47/299.88 , mark^#(tt()) -> c_8() 1178.47/299.88 , mark^#(cons(X1, X2)) -> c_9(mark^#(X1), X2) 1178.47/299.88 , mark^#(natsFrom(X)) -> c_10(a__natsFrom^#(mark(X))) 1178.47/299.88 , mark^#(s(X)) -> c_11(mark^#(X)) 1178.47/299.88 , mark^#(pair(X1, X2)) -> c_12(mark^#(X1), mark^#(X2)) 1178.47/299.88 , mark^#(nil()) -> c_13() 1178.47/299.88 , mark^#(isLNat(X)) -> c_14(a__isLNat^#(X)) 1178.47/299.88 , mark^#(afterNth(X1, X2)) -> 1178.47/299.88 c_15(a__afterNth^#(mark(X1), mark(X2))) 1178.47/299.88 , mark^#(fst(X)) -> c_16(a__fst^#(mark(X))) 1178.47/299.88 , mark^#(snd(X)) -> c_17(a__snd^#(mark(X))) 1178.47/299.88 , mark^#(tail(X)) -> c_18(a__tail^#(mark(X))) 1178.47/299.88 , mark^#(take(X1, X2)) -> c_19(a__take^#(mark(X1), mark(X2))) 1178.47/299.88 , mark^#(0()) -> c_20() 1178.47/299.88 , mark^#(head(X)) -> c_21(a__head^#(mark(X))) 1178.47/299.88 , mark^#(sel(X1, X2)) -> c_22(a__sel^#(mark(X1), mark(X2))) 1178.47/299.89 , mark^#(splitAt(X1, X2)) -> c_23(a__splitAt^#(mark(X1), mark(X2))) 1178.47/299.89 , mark^#(and(X1, X2)) -> c_24(a__and^#(mark(X1), X2)) 1178.47/299.89 , mark^#(isNatural(X)) -> c_25(a__isNatural^#(X)) 1178.47/299.89 , mark^#(U101(X1, X2, X3)) -> c_26(a__U101^#(mark(X1), X2, X3)) 1178.47/299.89 , mark^#(U11(X1, X2, X3)) -> c_27(a__U11^#(mark(X1), X2, X3)) 1178.47/299.89 , mark^#(U21(X1, X2)) -> c_28(a__U21^#(mark(X1), X2)) 1178.47/299.89 , mark^#(U31(X1, X2)) -> c_29(a__U31^#(mark(X1), X2)) 1178.47/299.89 , mark^#(U41(X1, X2)) -> c_30(a__U41^#(mark(X1), X2)) 1178.47/299.89 , mark^#(U51(X1, X2, X3)) -> c_31(a__U51^#(mark(X1), X2, X3)) 1178.47/299.89 , mark^#(U61(X1, X2)) -> c_32(a__U61^#(mark(X1), X2)) 1178.47/299.89 , mark^#(U71(X1, X2)) -> c_33(a__U71^#(mark(X1), X2)) 1178.47/299.89 , mark^#(U81(X1, X2, X3, X4)) -> 1178.47/299.89 c_34(a__U81^#(mark(X1), X2, X3, X4)) 1178.47/299.89 , mark^#(U82(X1, X2)) -> c_35(a__U82^#(mark(X1), X2)) 1178.47/299.89 , mark^#(U91(X1, X2)) -> c_36(a__U91^#(mark(X1), X2)) 1178.47/299.89 , mark^#(isPLNat(X)) -> c_37(a__isPLNat^#(X)) 1178.47/299.89 , a__natsFrom^#(N) -> c_83(a__U41^#(a__isNatural(N), N)) 1178.47/299.89 , a__natsFrom^#(X) -> c_84(X) 1178.47/299.89 , a__isLNat^#(X) -> c_71(X) 1178.47/299.89 , a__isLNat^#(cons(V1, V2)) -> 1178.47/299.89 c_72(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.47/299.89 , a__isLNat^#(natsFrom(V1)) -> c_73(a__isNatural^#(V1)) 1178.47/299.89 , a__isLNat^#(nil()) -> c_74() 1178.47/299.89 , a__isLNat^#(afterNth(V1, V2)) -> 1178.47/299.89 c_75(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.47/299.89 , a__isLNat^#(fst(V1)) -> c_76(a__isPLNat^#(V1)) 1178.47/299.89 , a__isLNat^#(snd(V1)) -> c_77(a__isPLNat^#(V1)) 1178.47/299.89 , a__isLNat^#(tail(V1)) -> c_78(a__isLNat^#(V1)) 1178.47/299.89 , a__isLNat^#(take(V1, V2)) -> 1178.47/299.89 c_79(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.47/299.89 , a__afterNth^#(N, XS) -> 1178.47/299.89 c_52(a__U11^#(a__and(a__isNatural(N), isLNat(XS)), N, XS)) 1178.47/299.89 , a__afterNth^#(X1, X2) -> c_53(X1, X2) 1178.47/299.89 , a__snd^#(X) -> c_40(X) 1178.47/299.89 , a__snd^#(pair(X, Y)) -> 1178.47/299.89 c_41(a__U61^#(a__and(a__isLNat(X), isLNat(Y)), Y)) 1178.47/299.89 , a__tail^#(X) -> c_87(X) 1178.47/299.89 , a__tail^#(cons(N, XS)) -> 1178.47/299.89 c_88(a__U91^#(a__and(a__isNatural(N), isLNat(XS)), XS)) 1178.47/299.89 , a__take^#(N, XS) -> 1178.47/299.89 c_89(a__U101^#(a__and(a__isNatural(N), isLNat(XS)), N, XS)) 1178.47/299.89 , a__take^#(X1, X2) -> c_90(X1, X2) 1178.47/299.89 , a__head^#(X) -> c_50(X) 1178.47/299.89 , a__head^#(cons(N, XS)) -> 1178.47/299.89 c_51(a__U31^#(a__and(a__isNatural(N), isLNat(XS)), N)) 1178.47/299.89 , a__sel^#(N, XS) -> 1178.47/299.89 c_85(a__U51^#(a__and(a__isNatural(N), isLNat(XS)), N, XS)) 1178.47/299.89 , a__sel^#(X1, X2) -> c_86(X1, X2) 1178.47/299.89 , a__and^#(X1, X2) -> c_64(X1, X2) 1178.47/299.89 , a__and^#(tt(), X) -> c_65(mark^#(X)) 1178.47/299.89 , a__isNatural^#(X) -> c_66(X) 1178.47/299.89 , a__isNatural^#(s(V1)) -> c_67(a__isNatural^#(V1)) 1178.47/299.89 , a__isNatural^#(0()) -> c_68() 1178.47/299.89 , a__isNatural^#(head(V1)) -> c_69(a__isLNat^#(V1)) 1178.47/299.89 , a__isNatural^#(sel(V1, V2)) -> 1178.47/299.89 c_70(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.47/299.89 , a__U11^#(X1, X2, X3) -> c_38(X1, X2, X3) 1178.47/299.89 , a__U11^#(tt(), N, XS) -> 1178.47/299.89 c_39(a__snd^#(a__splitAt(mark(N), mark(XS)))) 1178.47/299.89 , a__U31^#(X1, X2) -> c_44(X1, X2) 1178.47/299.89 , a__U31^#(tt(), N) -> c_45(mark^#(N)) 1178.47/299.89 , a__U41^#(X1, X2) -> c_46(X1, X2) 1178.47/299.89 , a__U41^#(tt(), N) -> c_47(mark^#(N), N) 1178.47/299.89 , a__U51^#(X1, X2, X3) -> c_48(X1, X2, X3) 1178.47/299.89 , a__U51^#(tt(), N, XS) -> 1178.47/299.89 c_49(a__head^#(a__afterNth(mark(N), mark(XS)))) 1178.47/299.89 , a__U61^#(X1, X2) -> c_54(X1, X2) 1178.47/299.89 , a__U61^#(tt(), Y) -> c_55(mark^#(Y)) 1178.47/299.89 , a__U82^#(X1, X2) -> c_60(X1, X2) 1178.47/299.89 , a__U82^#(pair(YS, ZS), X) -> c_61(mark^#(X), YS, mark^#(ZS)) 1178.47/299.89 , a__U91^#(X1, X2) -> c_62(X1, X2) 1178.47/299.89 , a__U91^#(tt(), XS) -> c_63(mark^#(XS)) 1178.47/299.89 , a__isPLNat^#(X) -> c_80(X) 1178.47/299.89 , a__isPLNat^#(pair(V1, V2)) -> 1178.47/299.89 c_81(a__and^#(a__isLNat(V1), isLNat(V2))) 1178.47/299.89 , a__isPLNat^#(splitAt(V1, V2)) -> 1178.47/299.89 c_82(a__and^#(a__isNatural(V1), isLNat(V2))) } 1178.47/299.89 1178.47/299.89 and mark the set of starting terms. 1178.47/299.89 1178.47/299.89 We are left with following problem, upon which TcT provides the 1178.47/299.89 certificate MAYBE. 1178.47/299.89 1178.47/299.89 Strict DPs: 1178.47/299.89 { a__U101^#(X1, X2, X3) -> c_1(X1, X2, X3) 1178.47/299.89 , a__U101^#(tt(), N, XS) -> 1178.47/299.89 c_2(a__fst^#(a__splitAt(mark(N), mark(XS)))) 1178.47/299.89 , a__fst^#(X) -> c_3(X) 1178.47/299.89 , a__fst^#(pair(X, Y)) -> 1178.47/299.89 c_4(a__U21^#(a__and(a__isLNat(X), isLNat(Y)), X)) 1178.47/299.89 , a__U21^#(X1, X2) -> c_42(X1, X2) 1178.47/299.89 , a__U21^#(tt(), X) -> c_43(mark^#(X)) 1178.47/299.89 , a__splitAt^#(X1, X2) -> c_5(X1, X2) 1178.47/299.89 , a__splitAt^#(s(N), cons(X, XS)) -> 1178.47/299.89 c_6(a__U81^#(a__and(a__isNatural(N), 1178.47/299.89 and(isNatural(X), isLNat(XS))), 1178.47/299.89 N, 1178.47/299.89 X, 1178.47/299.89 XS)) 1178.47/299.89 , a__splitAt^#(0(), XS) -> c_7(a__U71^#(a__isLNat(XS), XS)) 1178.47/299.89 , a__U81^#(X1, X2, X3, X4) -> c_58(X1, X2, X3, X4) 1178.47/299.89 , a__U81^#(tt(), N, X, XS) -> 1178.47/299.89 c_59(a__U82^#(a__splitAt(mark(N), mark(XS)), X)) 1178.47/299.89 , a__U71^#(X1, X2) -> c_56(X1, X2) 1178.47/299.89 , a__U71^#(tt(), XS) -> c_57(mark^#(XS)) 1178.47/299.89 , mark^#(tt()) -> c_8() 1178.47/299.89 , mark^#(cons(X1, X2)) -> c_9(mark^#(X1), X2) 1178.47/299.89 , mark^#(natsFrom(X)) -> c_10(a__natsFrom^#(mark(X))) 1178.47/299.89 , mark^#(s(X)) -> c_11(mark^#(X)) 1178.47/299.89 , mark^#(pair(X1, X2)) -> c_12(mark^#(X1), mark^#(X2)) 1178.47/299.89 , mark^#(nil()) -> c_13() 1178.47/299.89 , mark^#(isLNat(X)) -> c_14(a__isLNat^#(X)) 1178.47/299.89 , mark^#(afterNth(X1, X2)) -> 1178.47/299.89 c_15(a__afterNth^#(mark(X1), mark(X2))) 1178.47/299.89 , mark^#(fst(X)) -> c_16(a__fst^#(mark(X))) 1178.47/299.89 , mark^#(snd(X)) -> c_17(a__snd^#(mark(X))) 1178.47/299.89 , mark^#(tail(X)) -> c_18(a__tail^#(mark(X))) 1178.47/299.89 , mark^#(take(X1, X2)) -> c_19(a__take^#(mark(X1), mark(X2))) 1178.47/299.89 , mark^#(0()) -> c_20() 1178.47/299.89 , mark^#(head(X)) -> c_21(a__head^#(mark(X))) 1178.47/299.89 , mark^#(sel(X1, X2)) -> c_22(a__sel^#(mark(X1), mark(X2))) 1178.47/299.89 , mark^#(splitAt(X1, X2)) -> c_23(a__splitAt^#(mark(X1), mark(X2))) 1178.47/299.89 , mark^#(and(X1, X2)) -> c_24(a__and^#(mark(X1), X2)) 1178.47/299.89 , mark^#(isNatural(X)) -> c_25(a__isNatural^#(X)) 1178.47/299.89 , mark^#(U101(X1, X2, X3)) -> c_26(a__U101^#(mark(X1), X2, X3)) 1178.47/299.89 , mark^#(U11(X1, X2, X3)) -> c_27(a__U11^#(mark(X1), X2, X3)) 1178.47/299.89 , mark^#(U21(X1, X2)) -> c_28(a__U21^#(mark(X1), X2)) 1178.47/299.89 , mark^#(U31(X1, X2)) -> c_29(a__U31^#(mark(X1), X2)) 1178.47/299.89 , mark^#(U41(X1, X2)) -> c_30(a__U41^#(mark(X1), X2)) 1178.47/299.89 , mark^#(U51(X1, X2, X3)) -> c_31(a__U51^#(mark(X1), X2, X3)) 1178.47/299.89 , mark^#(U61(X1, X2)) -> c_32(a__U61^#(mark(X1), X2)) 1178.47/299.89 , mark^#(U71(X1, X2)) -> c_33(a__U71^#(mark(X1), X2)) 1178.47/299.89 , mark^#(U81(X1, X2, X3, X4)) -> 1178.47/299.89 c_34(a__U81^#(mark(X1), X2, X3, X4)) 1178.47/299.89 , mark^#(U82(X1, X2)) -> c_35(a__U82^#(mark(X1), X2)) 1178.47/299.89 , mark^#(U91(X1, X2)) -> c_36(a__U91^#(mark(X1), X2)) 1178.47/299.89 , mark^#(isPLNat(X)) -> c_37(a__isPLNat^#(X)) 1178.47/299.89 , a__natsFrom^#(N) -> c_83(a__U41^#(a__isNatural(N), N)) 1178.47/299.89 , a__natsFrom^#(X) -> c_84(X) 1178.47/299.89 , a__isLNat^#(X) -> c_71(X) 1178.47/299.89 , a__isLNat^#(cons(V1, V2)) -> 1178.47/299.89 c_72(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.47/299.89 , a__isLNat^#(natsFrom(V1)) -> c_73(a__isNatural^#(V1)) 1178.47/299.89 , a__isLNat^#(nil()) -> c_74() 1178.47/299.89 , a__isLNat^#(afterNth(V1, V2)) -> 1178.47/299.89 c_75(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.47/299.89 , a__isLNat^#(fst(V1)) -> c_76(a__isPLNat^#(V1)) 1178.47/299.89 , a__isLNat^#(snd(V1)) -> c_77(a__isPLNat^#(V1)) 1178.47/299.89 , a__isLNat^#(tail(V1)) -> c_78(a__isLNat^#(V1)) 1178.47/299.89 , a__isLNat^#(take(V1, V2)) -> 1178.47/299.89 c_79(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.47/299.89 , a__afterNth^#(N, XS) -> 1178.47/299.89 c_52(a__U11^#(a__and(a__isNatural(N), isLNat(XS)), N, XS)) 1178.47/299.89 , a__afterNth^#(X1, X2) -> c_53(X1, X2) 1178.47/299.89 , a__snd^#(X) -> c_40(X) 1178.47/299.89 , a__snd^#(pair(X, Y)) -> 1178.47/299.89 c_41(a__U61^#(a__and(a__isLNat(X), isLNat(Y)), Y)) 1178.47/299.89 , a__tail^#(X) -> c_87(X) 1178.47/299.89 , a__tail^#(cons(N, XS)) -> 1178.47/299.89 c_88(a__U91^#(a__and(a__isNatural(N), isLNat(XS)), XS)) 1178.47/299.89 , a__take^#(N, XS) -> 1178.47/299.89 c_89(a__U101^#(a__and(a__isNatural(N), isLNat(XS)), N, XS)) 1178.47/299.89 , a__take^#(X1, X2) -> c_90(X1, X2) 1178.47/299.89 , a__head^#(X) -> c_50(X) 1178.47/299.89 , a__head^#(cons(N, XS)) -> 1178.47/299.89 c_51(a__U31^#(a__and(a__isNatural(N), isLNat(XS)), N)) 1178.47/299.89 , a__sel^#(N, XS) -> 1178.47/299.89 c_85(a__U51^#(a__and(a__isNatural(N), isLNat(XS)), N, XS)) 1178.47/299.89 , a__sel^#(X1, X2) -> c_86(X1, X2) 1178.47/299.89 , a__and^#(X1, X2) -> c_64(X1, X2) 1178.47/299.89 , a__and^#(tt(), X) -> c_65(mark^#(X)) 1178.47/299.89 , a__isNatural^#(X) -> c_66(X) 1178.47/299.89 , a__isNatural^#(s(V1)) -> c_67(a__isNatural^#(V1)) 1178.47/299.89 , a__isNatural^#(0()) -> c_68() 1178.47/299.89 , a__isNatural^#(head(V1)) -> c_69(a__isLNat^#(V1)) 1178.47/299.89 , a__isNatural^#(sel(V1, V2)) -> 1178.47/299.89 c_70(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.47/299.89 , a__U11^#(X1, X2, X3) -> c_38(X1, X2, X3) 1178.47/299.89 , a__U11^#(tt(), N, XS) -> 1178.47/299.89 c_39(a__snd^#(a__splitAt(mark(N), mark(XS)))) 1178.47/299.89 , a__U31^#(X1, X2) -> c_44(X1, X2) 1178.47/299.89 , a__U31^#(tt(), N) -> c_45(mark^#(N)) 1178.47/299.89 , a__U41^#(X1, X2) -> c_46(X1, X2) 1178.47/299.89 , a__U41^#(tt(), N) -> c_47(mark^#(N), N) 1178.47/299.89 , a__U51^#(X1, X2, X3) -> c_48(X1, X2, X3) 1178.47/299.89 , a__U51^#(tt(), N, XS) -> 1178.47/299.89 c_49(a__head^#(a__afterNth(mark(N), mark(XS)))) 1178.47/299.89 , a__U61^#(X1, X2) -> c_54(X1, X2) 1178.47/299.89 , a__U61^#(tt(), Y) -> c_55(mark^#(Y)) 1178.47/299.89 , a__U82^#(X1, X2) -> c_60(X1, X2) 1178.47/299.89 , a__U82^#(pair(YS, ZS), X) -> c_61(mark^#(X), YS, mark^#(ZS)) 1178.47/299.89 , a__U91^#(X1, X2) -> c_62(X1, X2) 1178.47/299.89 , a__U91^#(tt(), XS) -> c_63(mark^#(XS)) 1178.47/299.89 , a__isPLNat^#(X) -> c_80(X) 1178.47/299.89 , a__isPLNat^#(pair(V1, V2)) -> 1178.47/299.89 c_81(a__and^#(a__isLNat(V1), isLNat(V2))) 1178.47/299.89 , a__isPLNat^#(splitAt(V1, V2)) -> 1178.47/299.89 c_82(a__and^#(a__isNatural(V1), isLNat(V2))) } 1178.47/299.89 Strict Trs: 1178.47/299.89 { a__U101(X1, X2, X3) -> U101(X1, X2, X3) 1178.47/299.89 , a__U101(tt(), N, XS) -> a__fst(a__splitAt(mark(N), mark(XS))) 1178.47/299.89 , a__fst(X) -> fst(X) 1178.47/299.89 , a__fst(pair(X, Y)) -> a__U21(a__and(a__isLNat(X), isLNat(Y)), X) 1178.47/299.89 , a__splitAt(X1, X2) -> splitAt(X1, X2) 1178.47/299.89 , a__splitAt(s(N), cons(X, XS)) -> 1178.47/299.89 a__U81(a__and(a__isNatural(N), and(isNatural(X), isLNat(XS))), 1178.47/299.89 N, 1178.47/299.89 X, 1178.47/299.89 XS) 1178.47/299.89 , a__splitAt(0(), XS) -> a__U71(a__isLNat(XS), XS) 1178.47/299.89 , mark(tt()) -> tt() 1178.47/299.89 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 1178.47/299.89 , mark(natsFrom(X)) -> a__natsFrom(mark(X)) 1178.47/299.89 , mark(s(X)) -> s(mark(X)) 1178.47/299.89 , mark(pair(X1, X2)) -> pair(mark(X1), mark(X2)) 1178.47/299.89 , mark(nil()) -> nil() 1178.47/299.89 , mark(isLNat(X)) -> a__isLNat(X) 1178.47/299.89 , mark(afterNth(X1, X2)) -> a__afterNth(mark(X1), mark(X2)) 1178.47/299.89 , mark(fst(X)) -> a__fst(mark(X)) 1178.47/299.89 , mark(snd(X)) -> a__snd(mark(X)) 1178.47/299.89 , mark(tail(X)) -> a__tail(mark(X)) 1178.47/299.89 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 1178.47/299.89 , mark(0()) -> 0() 1178.47/299.89 , mark(head(X)) -> a__head(mark(X)) 1178.47/299.89 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1178.47/299.89 , mark(splitAt(X1, X2)) -> a__splitAt(mark(X1), mark(X2)) 1178.47/299.89 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1178.47/299.89 , mark(isNatural(X)) -> a__isNatural(X) 1178.47/299.89 , mark(U101(X1, X2, X3)) -> a__U101(mark(X1), X2, X3) 1178.47/299.89 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 1178.47/299.89 , mark(U21(X1, X2)) -> a__U21(mark(X1), X2) 1178.47/299.89 , mark(U31(X1, X2)) -> a__U31(mark(X1), X2) 1178.47/299.89 , mark(U41(X1, X2)) -> a__U41(mark(X1), X2) 1178.47/299.89 , mark(U51(X1, X2, X3)) -> a__U51(mark(X1), X2, X3) 1178.47/299.89 , mark(U61(X1, X2)) -> a__U61(mark(X1), X2) 1178.47/299.89 , mark(U71(X1, X2)) -> a__U71(mark(X1), X2) 1178.47/299.89 , mark(U81(X1, X2, X3, X4)) -> a__U81(mark(X1), X2, X3, X4) 1178.47/299.89 , mark(U82(X1, X2)) -> a__U82(mark(X1), X2) 1178.47/299.89 , mark(U91(X1, X2)) -> a__U91(mark(X1), X2) 1178.47/299.89 , mark(isPLNat(X)) -> a__isPLNat(X) 1178.47/299.89 , a__U11(X1, X2, X3) -> U11(X1, X2, X3) 1178.47/299.89 , a__U11(tt(), N, XS) -> a__snd(a__splitAt(mark(N), mark(XS))) 1178.47/299.89 , a__snd(X) -> snd(X) 1178.47/299.89 , a__snd(pair(X, Y)) -> a__U61(a__and(a__isLNat(X), isLNat(Y)), Y) 1178.47/299.89 , a__U21(X1, X2) -> U21(X1, X2) 1178.47/299.89 , a__U21(tt(), X) -> mark(X) 1178.47/299.89 , a__U31(X1, X2) -> U31(X1, X2) 1178.47/299.89 , a__U31(tt(), N) -> mark(N) 1178.47/299.89 , a__U41(X1, X2) -> U41(X1, X2) 1178.47/299.89 , a__U41(tt(), N) -> cons(mark(N), natsFrom(s(N))) 1178.47/299.89 , a__U51(X1, X2, X3) -> U51(X1, X2, X3) 1178.47/299.89 , a__U51(tt(), N, XS) -> a__head(a__afterNth(mark(N), mark(XS))) 1178.47/299.89 , a__head(X) -> head(X) 1178.47/299.89 , a__head(cons(N, XS)) -> 1178.47/299.89 a__U31(a__and(a__isNatural(N), isLNat(XS)), N) 1178.47/299.89 , a__afterNth(N, XS) -> 1178.47/299.89 a__U11(a__and(a__isNatural(N), isLNat(XS)), N, XS) 1178.47/299.89 , a__afterNth(X1, X2) -> afterNth(X1, X2) 1178.47/299.89 , a__U61(X1, X2) -> U61(X1, X2) 1178.47/299.89 , a__U61(tt(), Y) -> mark(Y) 1178.47/299.89 , a__U71(X1, X2) -> U71(X1, X2) 1178.47/299.89 , a__U71(tt(), XS) -> pair(nil(), mark(XS)) 1178.47/299.89 , a__U81(X1, X2, X3, X4) -> U81(X1, X2, X3, X4) 1178.47/299.89 , a__U81(tt(), N, X, XS) -> 1178.47/299.89 a__U82(a__splitAt(mark(N), mark(XS)), X) 1178.47/299.89 , a__U82(X1, X2) -> U82(X1, X2) 1178.47/299.89 , a__U82(pair(YS, ZS), X) -> pair(cons(mark(X), YS), mark(ZS)) 1178.47/299.89 , a__U91(X1, X2) -> U91(X1, X2) 1178.47/299.89 , a__U91(tt(), XS) -> mark(XS) 1178.47/299.89 , a__and(X1, X2) -> and(X1, X2) 1178.47/299.89 , a__and(tt(), X) -> mark(X) 1178.47/299.89 , a__isNatural(X) -> isNatural(X) 1178.47/299.89 , a__isNatural(s(V1)) -> a__isNatural(V1) 1178.47/299.89 , a__isNatural(0()) -> tt() 1178.47/299.89 , a__isNatural(head(V1)) -> a__isLNat(V1) 1178.47/299.89 , a__isNatural(sel(V1, V2)) -> a__and(a__isNatural(V1), isLNat(V2)) 1178.47/299.89 , a__isLNat(X) -> isLNat(X) 1178.47/299.89 , a__isLNat(cons(V1, V2)) -> a__and(a__isNatural(V1), isLNat(V2)) 1178.47/299.89 , a__isLNat(natsFrom(V1)) -> a__isNatural(V1) 1178.47/299.89 , a__isLNat(nil()) -> tt() 1178.47/299.89 , a__isLNat(afterNth(V1, V2)) -> 1178.47/299.89 a__and(a__isNatural(V1), isLNat(V2)) 1178.47/299.89 , a__isLNat(fst(V1)) -> a__isPLNat(V1) 1178.47/299.89 , a__isLNat(snd(V1)) -> a__isPLNat(V1) 1178.47/299.89 , a__isLNat(tail(V1)) -> a__isLNat(V1) 1178.47/299.89 , a__isLNat(take(V1, V2)) -> a__and(a__isNatural(V1), isLNat(V2)) 1178.47/299.89 , a__isPLNat(X) -> isPLNat(X) 1178.47/299.89 , a__isPLNat(pair(V1, V2)) -> a__and(a__isLNat(V1), isLNat(V2)) 1178.47/299.89 , a__isPLNat(splitAt(V1, V2)) -> 1178.47/299.89 a__and(a__isNatural(V1), isLNat(V2)) 1178.47/299.89 , a__natsFrom(N) -> a__U41(a__isNatural(N), N) 1178.47/299.89 , a__natsFrom(X) -> natsFrom(X) 1178.47/299.89 , a__sel(N, XS) -> 1178.47/299.89 a__U51(a__and(a__isNatural(N), isLNat(XS)), N, XS) 1178.47/299.89 , a__sel(X1, X2) -> sel(X1, X2) 1178.47/299.89 , a__tail(X) -> tail(X) 1178.47/299.89 , a__tail(cons(N, XS)) -> 1178.47/299.89 a__U91(a__and(a__isNatural(N), isLNat(XS)), XS) 1178.47/299.89 , a__take(N, XS) -> 1178.47/299.89 a__U101(a__and(a__isNatural(N), isLNat(XS)), N, XS) 1178.47/299.89 , a__take(X1, X2) -> take(X1, X2) } 1178.47/299.89 Obligation: 1178.47/299.89 runtime complexity 1178.47/299.89 Answer: 1178.47/299.89 MAYBE 1178.47/299.89 1178.47/299.89 We estimate the number of application of {14,19,26,49,71} by 1178.47/299.89 applications of Pre({14,19,26,49,71}) = 1178.47/299.89 {1,3,5,6,7,10,12,13,15,17,18,20,31,45,46,48,53,56,57,59,62,63,66,67,68,69,70,72,74,76,77,78,79,80,82,83,84,85,86,87,88}. 1178.47/299.89 Here rules are labeled as follows: 1178.47/299.89 1178.47/299.89 DPs: 1178.47/299.89 { 1: a__U101^#(X1, X2, X3) -> c_1(X1, X2, X3) 1178.47/299.89 , 2: a__U101^#(tt(), N, XS) -> 1178.47/299.89 c_2(a__fst^#(a__splitAt(mark(N), mark(XS)))) 1178.47/299.89 , 3: a__fst^#(X) -> c_3(X) 1178.47/299.89 , 4: a__fst^#(pair(X, Y)) -> 1178.47/299.89 c_4(a__U21^#(a__and(a__isLNat(X), isLNat(Y)), X)) 1178.47/299.89 , 5: a__U21^#(X1, X2) -> c_42(X1, X2) 1178.47/299.89 , 6: a__U21^#(tt(), X) -> c_43(mark^#(X)) 1178.47/299.89 , 7: a__splitAt^#(X1, X2) -> c_5(X1, X2) 1178.47/299.89 , 8: a__splitAt^#(s(N), cons(X, XS)) -> 1178.47/299.89 c_6(a__U81^#(a__and(a__isNatural(N), 1178.47/299.89 and(isNatural(X), isLNat(XS))), 1178.47/299.89 N, 1178.47/299.89 X, 1178.47/299.89 XS)) 1178.47/299.89 , 9: a__splitAt^#(0(), XS) -> c_7(a__U71^#(a__isLNat(XS), XS)) 1178.47/299.89 , 10: a__U81^#(X1, X2, X3, X4) -> c_58(X1, X2, X3, X4) 1178.47/299.89 , 11: a__U81^#(tt(), N, X, XS) -> 1178.47/299.89 c_59(a__U82^#(a__splitAt(mark(N), mark(XS)), X)) 1178.47/299.89 , 12: a__U71^#(X1, X2) -> c_56(X1, X2) 1178.47/299.89 , 13: a__U71^#(tt(), XS) -> c_57(mark^#(XS)) 1178.47/299.89 , 14: mark^#(tt()) -> c_8() 1178.47/299.89 , 15: mark^#(cons(X1, X2)) -> c_9(mark^#(X1), X2) 1178.47/299.89 , 16: mark^#(natsFrom(X)) -> c_10(a__natsFrom^#(mark(X))) 1178.47/299.89 , 17: mark^#(s(X)) -> c_11(mark^#(X)) 1178.47/299.89 , 18: mark^#(pair(X1, X2)) -> c_12(mark^#(X1), mark^#(X2)) 1178.47/299.89 , 19: mark^#(nil()) -> c_13() 1178.47/299.89 , 20: mark^#(isLNat(X)) -> c_14(a__isLNat^#(X)) 1178.47/299.89 , 21: mark^#(afterNth(X1, X2)) -> 1178.47/299.89 c_15(a__afterNth^#(mark(X1), mark(X2))) 1178.47/299.89 , 22: mark^#(fst(X)) -> c_16(a__fst^#(mark(X))) 1178.47/299.89 , 23: mark^#(snd(X)) -> c_17(a__snd^#(mark(X))) 1178.47/299.89 , 24: mark^#(tail(X)) -> c_18(a__tail^#(mark(X))) 1178.47/299.89 , 25: mark^#(take(X1, X2)) -> c_19(a__take^#(mark(X1), mark(X2))) 1178.47/299.89 , 26: mark^#(0()) -> c_20() 1178.47/299.89 , 27: mark^#(head(X)) -> c_21(a__head^#(mark(X))) 1178.47/299.89 , 28: mark^#(sel(X1, X2)) -> c_22(a__sel^#(mark(X1), mark(X2))) 1178.47/299.89 , 29: mark^#(splitAt(X1, X2)) -> 1178.47/299.89 c_23(a__splitAt^#(mark(X1), mark(X2))) 1178.47/299.89 , 30: mark^#(and(X1, X2)) -> c_24(a__and^#(mark(X1), X2)) 1178.47/299.89 , 31: mark^#(isNatural(X)) -> c_25(a__isNatural^#(X)) 1178.87/299.91 , 32: mark^#(U101(X1, X2, X3)) -> c_26(a__U101^#(mark(X1), X2, X3)) 1178.87/299.91 , 33: mark^#(U11(X1, X2, X3)) -> c_27(a__U11^#(mark(X1), X2, X3)) 1178.87/299.91 , 34: mark^#(U21(X1, X2)) -> c_28(a__U21^#(mark(X1), X2)) 1178.87/299.91 , 35: mark^#(U31(X1, X2)) -> c_29(a__U31^#(mark(X1), X2)) 1178.87/299.91 , 36: mark^#(U41(X1, X2)) -> c_30(a__U41^#(mark(X1), X2)) 1178.87/299.91 , 37: mark^#(U51(X1, X2, X3)) -> c_31(a__U51^#(mark(X1), X2, X3)) 1178.87/299.91 , 38: mark^#(U61(X1, X2)) -> c_32(a__U61^#(mark(X1), X2)) 1178.87/299.91 , 39: mark^#(U71(X1, X2)) -> c_33(a__U71^#(mark(X1), X2)) 1178.87/299.91 , 40: mark^#(U81(X1, X2, X3, X4)) -> 1178.87/299.91 c_34(a__U81^#(mark(X1), X2, X3, X4)) 1178.87/299.91 , 41: mark^#(U82(X1, X2)) -> c_35(a__U82^#(mark(X1), X2)) 1178.87/299.91 , 42: mark^#(U91(X1, X2)) -> c_36(a__U91^#(mark(X1), X2)) 1178.87/299.91 , 43: mark^#(isPLNat(X)) -> c_37(a__isPLNat^#(X)) 1178.87/299.91 , 44: a__natsFrom^#(N) -> c_83(a__U41^#(a__isNatural(N), N)) 1178.87/299.91 , 45: a__natsFrom^#(X) -> c_84(X) 1178.87/299.91 , 46: a__isLNat^#(X) -> c_71(X) 1178.87/299.91 , 47: a__isLNat^#(cons(V1, V2)) -> 1178.87/299.91 c_72(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.87/299.91 , 48: a__isLNat^#(natsFrom(V1)) -> c_73(a__isNatural^#(V1)) 1178.87/299.91 , 49: a__isLNat^#(nil()) -> c_74() 1178.87/299.91 , 50: a__isLNat^#(afterNth(V1, V2)) -> 1178.87/299.91 c_75(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.87/299.91 , 51: a__isLNat^#(fst(V1)) -> c_76(a__isPLNat^#(V1)) 1178.87/299.91 , 52: a__isLNat^#(snd(V1)) -> c_77(a__isPLNat^#(V1)) 1178.87/299.91 , 53: a__isLNat^#(tail(V1)) -> c_78(a__isLNat^#(V1)) 1178.87/299.91 , 54: a__isLNat^#(take(V1, V2)) -> 1178.87/299.91 c_79(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.87/299.91 , 55: a__afterNth^#(N, XS) -> 1178.87/299.91 c_52(a__U11^#(a__and(a__isNatural(N), isLNat(XS)), N, XS)) 1178.87/299.91 , 56: a__afterNth^#(X1, X2) -> c_53(X1, X2) 1178.87/299.91 , 57: a__snd^#(X) -> c_40(X) 1178.87/299.91 , 58: a__snd^#(pair(X, Y)) -> 1178.87/299.91 c_41(a__U61^#(a__and(a__isLNat(X), isLNat(Y)), Y)) 1178.87/299.91 , 59: a__tail^#(X) -> c_87(X) 1178.87/299.91 , 60: a__tail^#(cons(N, XS)) -> 1178.87/299.91 c_88(a__U91^#(a__and(a__isNatural(N), isLNat(XS)), XS)) 1178.87/299.91 , 61: a__take^#(N, XS) -> 1178.87/299.91 c_89(a__U101^#(a__and(a__isNatural(N), isLNat(XS)), N, XS)) 1178.87/299.91 , 62: a__take^#(X1, X2) -> c_90(X1, X2) 1178.87/299.91 , 63: a__head^#(X) -> c_50(X) 1178.87/299.91 , 64: a__head^#(cons(N, XS)) -> 1178.87/299.91 c_51(a__U31^#(a__and(a__isNatural(N), isLNat(XS)), N)) 1178.87/299.91 , 65: a__sel^#(N, XS) -> 1178.87/299.91 c_85(a__U51^#(a__and(a__isNatural(N), isLNat(XS)), N, XS)) 1178.87/299.91 , 66: a__sel^#(X1, X2) -> c_86(X1, X2) 1178.87/299.91 , 67: a__and^#(X1, X2) -> c_64(X1, X2) 1178.87/299.91 , 68: a__and^#(tt(), X) -> c_65(mark^#(X)) 1178.87/299.91 , 69: a__isNatural^#(X) -> c_66(X) 1178.87/299.91 , 70: a__isNatural^#(s(V1)) -> c_67(a__isNatural^#(V1)) 1178.87/299.91 , 71: a__isNatural^#(0()) -> c_68() 1178.87/299.91 , 72: a__isNatural^#(head(V1)) -> c_69(a__isLNat^#(V1)) 1178.87/299.91 , 73: a__isNatural^#(sel(V1, V2)) -> 1178.87/299.91 c_70(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.87/299.91 , 74: a__U11^#(X1, X2, X3) -> c_38(X1, X2, X3) 1178.87/299.91 , 75: a__U11^#(tt(), N, XS) -> 1178.87/299.91 c_39(a__snd^#(a__splitAt(mark(N), mark(XS)))) 1178.87/299.91 , 76: a__U31^#(X1, X2) -> c_44(X1, X2) 1178.87/299.91 , 77: a__U31^#(tt(), N) -> c_45(mark^#(N)) 1178.87/299.91 , 78: a__U41^#(X1, X2) -> c_46(X1, X2) 1178.87/299.91 , 79: a__U41^#(tt(), N) -> c_47(mark^#(N), N) 1178.87/299.91 , 80: a__U51^#(X1, X2, X3) -> c_48(X1, X2, X3) 1178.87/299.91 , 81: a__U51^#(tt(), N, XS) -> 1178.87/299.91 c_49(a__head^#(a__afterNth(mark(N), mark(XS)))) 1178.87/299.91 , 82: a__U61^#(X1, X2) -> c_54(X1, X2) 1178.87/299.91 , 83: a__U61^#(tt(), Y) -> c_55(mark^#(Y)) 1178.87/299.91 , 84: a__U82^#(X1, X2) -> c_60(X1, X2) 1178.87/299.91 , 85: a__U82^#(pair(YS, ZS), X) -> c_61(mark^#(X), YS, mark^#(ZS)) 1178.87/299.91 , 86: a__U91^#(X1, X2) -> c_62(X1, X2) 1178.87/299.91 , 87: a__U91^#(tt(), XS) -> c_63(mark^#(XS)) 1178.87/299.91 , 88: a__isPLNat^#(X) -> c_80(X) 1178.87/299.91 , 89: a__isPLNat^#(pair(V1, V2)) -> 1178.87/299.91 c_81(a__and^#(a__isLNat(V1), isLNat(V2))) 1178.87/299.91 , 90: a__isPLNat^#(splitAt(V1, V2)) -> 1178.87/299.91 c_82(a__and^#(a__isNatural(V1), isLNat(V2))) } 1178.87/299.91 1178.87/299.91 We are left with following problem, upon which TcT provides the 1178.87/299.91 certificate MAYBE. 1178.87/299.91 1178.87/299.91 Strict DPs: 1178.87/299.91 { a__U101^#(X1, X2, X3) -> c_1(X1, X2, X3) 1178.87/299.91 , a__U101^#(tt(), N, XS) -> 1178.87/299.91 c_2(a__fst^#(a__splitAt(mark(N), mark(XS)))) 1178.87/299.91 , a__fst^#(X) -> c_3(X) 1178.87/299.91 , a__fst^#(pair(X, Y)) -> 1178.87/299.91 c_4(a__U21^#(a__and(a__isLNat(X), isLNat(Y)), X)) 1178.87/299.91 , a__U21^#(X1, X2) -> c_42(X1, X2) 1178.87/299.91 , a__U21^#(tt(), X) -> c_43(mark^#(X)) 1178.87/299.91 , a__splitAt^#(X1, X2) -> c_5(X1, X2) 1178.87/299.91 , a__splitAt^#(s(N), cons(X, XS)) -> 1178.87/299.91 c_6(a__U81^#(a__and(a__isNatural(N), 1178.87/299.91 and(isNatural(X), isLNat(XS))), 1178.87/299.91 N, 1178.87/299.91 X, 1178.87/299.91 XS)) 1178.87/299.91 , a__splitAt^#(0(), XS) -> c_7(a__U71^#(a__isLNat(XS), XS)) 1178.87/299.91 , a__U81^#(X1, X2, X3, X4) -> c_58(X1, X2, X3, X4) 1178.87/299.91 , a__U81^#(tt(), N, X, XS) -> 1178.87/299.91 c_59(a__U82^#(a__splitAt(mark(N), mark(XS)), X)) 1178.87/299.91 , a__U71^#(X1, X2) -> c_56(X1, X2) 1178.87/299.91 , a__U71^#(tt(), XS) -> c_57(mark^#(XS)) 1178.87/299.91 , mark^#(cons(X1, X2)) -> c_9(mark^#(X1), X2) 1178.87/299.91 , mark^#(natsFrom(X)) -> c_10(a__natsFrom^#(mark(X))) 1178.87/299.91 , mark^#(s(X)) -> c_11(mark^#(X)) 1178.87/299.91 , mark^#(pair(X1, X2)) -> c_12(mark^#(X1), mark^#(X2)) 1178.87/299.91 , mark^#(isLNat(X)) -> c_14(a__isLNat^#(X)) 1178.87/299.91 , mark^#(afterNth(X1, X2)) -> 1178.87/299.91 c_15(a__afterNth^#(mark(X1), mark(X2))) 1178.87/299.91 , mark^#(fst(X)) -> c_16(a__fst^#(mark(X))) 1178.87/299.91 , mark^#(snd(X)) -> c_17(a__snd^#(mark(X))) 1178.87/299.91 , mark^#(tail(X)) -> c_18(a__tail^#(mark(X))) 1178.87/299.91 , mark^#(take(X1, X2)) -> c_19(a__take^#(mark(X1), mark(X2))) 1178.87/299.91 , mark^#(head(X)) -> c_21(a__head^#(mark(X))) 1178.87/299.91 , mark^#(sel(X1, X2)) -> c_22(a__sel^#(mark(X1), mark(X2))) 1178.87/299.91 , mark^#(splitAt(X1, X2)) -> c_23(a__splitAt^#(mark(X1), mark(X2))) 1178.87/299.91 , mark^#(and(X1, X2)) -> c_24(a__and^#(mark(X1), X2)) 1178.87/299.91 , mark^#(isNatural(X)) -> c_25(a__isNatural^#(X)) 1178.87/299.91 , mark^#(U101(X1, X2, X3)) -> c_26(a__U101^#(mark(X1), X2, X3)) 1178.87/299.91 , mark^#(U11(X1, X2, X3)) -> c_27(a__U11^#(mark(X1), X2, X3)) 1178.87/299.91 , mark^#(U21(X1, X2)) -> c_28(a__U21^#(mark(X1), X2)) 1178.87/299.91 , mark^#(U31(X1, X2)) -> c_29(a__U31^#(mark(X1), X2)) 1178.87/299.91 , mark^#(U41(X1, X2)) -> c_30(a__U41^#(mark(X1), X2)) 1178.87/299.91 , mark^#(U51(X1, X2, X3)) -> c_31(a__U51^#(mark(X1), X2, X3)) 1178.87/299.91 , mark^#(U61(X1, X2)) -> c_32(a__U61^#(mark(X1), X2)) 1178.87/299.91 , mark^#(U71(X1, X2)) -> c_33(a__U71^#(mark(X1), X2)) 1178.87/299.91 , mark^#(U81(X1, X2, X3, X4)) -> 1178.87/299.91 c_34(a__U81^#(mark(X1), X2, X3, X4)) 1178.87/299.91 , mark^#(U82(X1, X2)) -> c_35(a__U82^#(mark(X1), X2)) 1178.87/299.91 , mark^#(U91(X1, X2)) -> c_36(a__U91^#(mark(X1), X2)) 1178.87/299.91 , mark^#(isPLNat(X)) -> c_37(a__isPLNat^#(X)) 1178.87/299.91 , a__natsFrom^#(N) -> c_83(a__U41^#(a__isNatural(N), N)) 1178.87/299.91 , a__natsFrom^#(X) -> c_84(X) 1178.87/299.91 , a__isLNat^#(X) -> c_71(X) 1178.87/299.91 , a__isLNat^#(cons(V1, V2)) -> 1178.87/299.91 c_72(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.87/299.91 , a__isLNat^#(natsFrom(V1)) -> c_73(a__isNatural^#(V1)) 1178.87/299.91 , a__isLNat^#(afterNth(V1, V2)) -> 1178.87/299.91 c_75(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.87/299.91 , a__isLNat^#(fst(V1)) -> c_76(a__isPLNat^#(V1)) 1178.87/299.91 , a__isLNat^#(snd(V1)) -> c_77(a__isPLNat^#(V1)) 1178.87/299.91 , a__isLNat^#(tail(V1)) -> c_78(a__isLNat^#(V1)) 1178.87/299.91 , a__isLNat^#(take(V1, V2)) -> 1178.87/299.91 c_79(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.87/299.91 , a__afterNth^#(N, XS) -> 1178.87/299.91 c_52(a__U11^#(a__and(a__isNatural(N), isLNat(XS)), N, XS)) 1178.87/299.91 , a__afterNth^#(X1, X2) -> c_53(X1, X2) 1178.87/299.91 , a__snd^#(X) -> c_40(X) 1178.87/299.91 , a__snd^#(pair(X, Y)) -> 1178.87/299.91 c_41(a__U61^#(a__and(a__isLNat(X), isLNat(Y)), Y)) 1178.87/299.91 , a__tail^#(X) -> c_87(X) 1178.87/299.91 , a__tail^#(cons(N, XS)) -> 1178.87/299.91 c_88(a__U91^#(a__and(a__isNatural(N), isLNat(XS)), XS)) 1178.87/299.91 , a__take^#(N, XS) -> 1178.87/299.91 c_89(a__U101^#(a__and(a__isNatural(N), isLNat(XS)), N, XS)) 1178.87/299.91 , a__take^#(X1, X2) -> c_90(X1, X2) 1178.87/299.91 , a__head^#(X) -> c_50(X) 1178.87/299.91 , a__head^#(cons(N, XS)) -> 1178.87/299.91 c_51(a__U31^#(a__and(a__isNatural(N), isLNat(XS)), N)) 1178.87/299.91 , a__sel^#(N, XS) -> 1178.87/299.91 c_85(a__U51^#(a__and(a__isNatural(N), isLNat(XS)), N, XS)) 1178.87/299.91 , a__sel^#(X1, X2) -> c_86(X1, X2) 1178.87/299.91 , a__and^#(X1, X2) -> c_64(X1, X2) 1178.87/299.91 , a__and^#(tt(), X) -> c_65(mark^#(X)) 1178.87/299.91 , a__isNatural^#(X) -> c_66(X) 1178.87/299.91 , a__isNatural^#(s(V1)) -> c_67(a__isNatural^#(V1)) 1178.87/299.94 , a__isNatural^#(head(V1)) -> c_69(a__isLNat^#(V1)) 1178.87/299.94 , a__isNatural^#(sel(V1, V2)) -> 1178.87/299.94 c_70(a__and^#(a__isNatural(V1), isLNat(V2))) 1178.87/299.94 , a__U11^#(X1, X2, X3) -> c_38(X1, X2, X3) 1178.87/299.94 , a__U11^#(tt(), N, XS) -> 1178.87/299.94 c_39(a__snd^#(a__splitAt(mark(N), mark(XS)))) 1178.87/299.94 , a__U31^#(X1, X2) -> c_44(X1, X2) 1178.87/299.94 , a__U31^#(tt(), N) -> c_45(mark^#(N)) 1178.87/299.94 , a__U41^#(X1, X2) -> c_46(X1, X2) 1178.87/299.94 , a__U41^#(tt(), N) -> c_47(mark^#(N), N) 1178.87/299.94 , a__U51^#(X1, X2, X3) -> c_48(X1, X2, X3) 1178.87/299.94 , a__U51^#(tt(), N, XS) -> 1178.87/299.94 c_49(a__head^#(a__afterNth(mark(N), mark(XS)))) 1178.87/299.94 , a__U61^#(X1, X2) -> c_54(X1, X2) 1178.87/299.94 , a__U61^#(tt(), Y) -> c_55(mark^#(Y)) 1178.87/299.94 , a__U82^#(X1, X2) -> c_60(X1, X2) 1178.87/299.94 , a__U82^#(pair(YS, ZS), X) -> c_61(mark^#(X), YS, mark^#(ZS)) 1178.87/299.94 , a__U91^#(X1, X2) -> c_62(X1, X2) 1178.87/299.94 , a__U91^#(tt(), XS) -> c_63(mark^#(XS)) 1178.87/299.94 , a__isPLNat^#(X) -> c_80(X) 1178.87/299.94 , a__isPLNat^#(pair(V1, V2)) -> 1178.87/299.94 c_81(a__and^#(a__isLNat(V1), isLNat(V2))) 1178.87/299.94 , a__isPLNat^#(splitAt(V1, V2)) -> 1178.87/299.94 c_82(a__and^#(a__isNatural(V1), isLNat(V2))) } 1178.87/299.94 Strict Trs: 1178.87/299.94 { a__U101(X1, X2, X3) -> U101(X1, X2, X3) 1178.87/299.94 , a__U101(tt(), N, XS) -> a__fst(a__splitAt(mark(N), mark(XS))) 1178.87/299.94 , a__fst(X) -> fst(X) 1178.87/299.94 , a__fst(pair(X, Y)) -> a__U21(a__and(a__isLNat(X), isLNat(Y)), X) 1178.87/299.94 , a__splitAt(X1, X2) -> splitAt(X1, X2) 1178.87/299.94 , a__splitAt(s(N), cons(X, XS)) -> 1178.87/299.94 a__U81(a__and(a__isNatural(N), and(isNatural(X), isLNat(XS))), 1178.87/299.94 N, 1178.87/299.94 X, 1178.87/299.94 XS) 1178.87/299.94 , a__splitAt(0(), XS) -> a__U71(a__isLNat(XS), XS) 1178.87/299.94 , mark(tt()) -> tt() 1178.87/299.94 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 1178.87/299.94 , mark(natsFrom(X)) -> a__natsFrom(mark(X)) 1178.87/299.94 , mark(s(X)) -> s(mark(X)) 1178.87/299.94 , mark(pair(X1, X2)) -> pair(mark(X1), mark(X2)) 1178.87/299.94 , mark(nil()) -> nil() 1178.87/299.94 , mark(isLNat(X)) -> a__isLNat(X) 1178.87/299.94 , mark(afterNth(X1, X2)) -> a__afterNth(mark(X1), mark(X2)) 1178.87/299.94 , mark(fst(X)) -> a__fst(mark(X)) 1178.87/299.94 , mark(snd(X)) -> a__snd(mark(X)) 1178.87/299.94 , mark(tail(X)) -> a__tail(mark(X)) 1178.87/299.94 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 1178.87/299.94 , mark(0()) -> 0() 1178.87/299.94 , mark(head(X)) -> a__head(mark(X)) 1178.87/299.94 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1178.87/299.94 , mark(splitAt(X1, X2)) -> a__splitAt(mark(X1), mark(X2)) 1178.87/299.94 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1178.87/299.94 , mark(isNatural(X)) -> a__isNatural(X) 1178.87/299.94 , mark(U101(X1, X2, X3)) -> a__U101(mark(X1), X2, X3) 1178.87/299.94 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 1178.87/299.94 , mark(U21(X1, X2)) -> a__U21(mark(X1), X2) 1178.87/299.94 , mark(U31(X1, X2)) -> a__U31(mark(X1), X2) 1178.87/299.94 , mark(U41(X1, X2)) -> a__U41(mark(X1), X2) 1178.87/299.94 , mark(U51(X1, X2, X3)) -> a__U51(mark(X1), X2, X3) 1178.87/299.94 , mark(U61(X1, X2)) -> a__U61(mark(X1), X2) 1178.87/299.94 , mark(U71(X1, X2)) -> a__U71(mark(X1), X2) 1178.87/299.94 , mark(U81(X1, X2, X3, X4)) -> a__U81(mark(X1), X2, X3, X4) 1178.87/299.94 , mark(U82(X1, X2)) -> a__U82(mark(X1), X2) 1178.87/299.94 , mark(U91(X1, X2)) -> a__U91(mark(X1), X2) 1178.87/299.94 , mark(isPLNat(X)) -> a__isPLNat(X) 1178.87/299.94 , a__U11(X1, X2, X3) -> U11(X1, X2, X3) 1178.87/299.94 , a__U11(tt(), N, XS) -> a__snd(a__splitAt(mark(N), mark(XS))) 1178.87/299.94 , a__snd(X) -> snd(X) 1178.87/299.94 , a__snd(pair(X, Y)) -> a__U61(a__and(a__isLNat(X), isLNat(Y)), Y) 1178.87/299.94 , a__U21(X1, X2) -> U21(X1, X2) 1178.87/299.94 , a__U21(tt(), X) -> mark(X) 1178.87/299.94 , a__U31(X1, X2) -> U31(X1, X2) 1178.87/299.94 , a__U31(tt(), N) -> mark(N) 1178.87/299.94 , a__U41(X1, X2) -> U41(X1, X2) 1178.87/299.94 , a__U41(tt(), N) -> cons(mark(N), natsFrom(s(N))) 1178.87/299.94 , a__U51(X1, X2, X3) -> U51(X1, X2, X3) 1178.87/299.94 , a__U51(tt(), N, XS) -> a__head(a__afterNth(mark(N), mark(XS))) 1178.87/299.94 , a__head(X) -> head(X) 1178.87/299.94 , a__head(cons(N, XS)) -> 1178.87/299.94 a__U31(a__and(a__isNatural(N), isLNat(XS)), N) 1178.87/299.94 , a__afterNth(N, XS) -> 1178.87/299.94 a__U11(a__and(a__isNatural(N), isLNat(XS)), N, XS) 1178.87/299.94 , a__afterNth(X1, X2) -> afterNth(X1, X2) 1178.87/299.94 , a__U61(X1, X2) -> U61(X1, X2) 1178.87/299.94 , a__U61(tt(), Y) -> mark(Y) 1178.87/299.94 , a__U71(X1, X2) -> U71(X1, X2) 1178.87/299.94 , a__U71(tt(), XS) -> pair(nil(), mark(XS)) 1178.87/299.94 , a__U81(X1, X2, X3, X4) -> U81(X1, X2, X3, X4) 1178.87/299.94 , a__U81(tt(), N, X, XS) -> 1178.87/299.94 a__U82(a__splitAt(mark(N), mark(XS)), X) 1178.87/299.94 , a__U82(X1, X2) -> U82(X1, X2) 1178.87/299.94 , a__U82(pair(YS, ZS), X) -> pair(cons(mark(X), YS), mark(ZS)) 1178.87/299.94 , a__U91(X1, X2) -> U91(X1, X2) 1178.87/299.94 , a__U91(tt(), XS) -> mark(XS) 1178.87/299.94 , a__and(X1, X2) -> and(X1, X2) 1178.87/299.94 , a__and(tt(), X) -> mark(X) 1178.87/299.94 , a__isNatural(X) -> isNatural(X) 1178.87/299.94 , a__isNatural(s(V1)) -> a__isNatural(V1) 1178.87/299.94 , a__isNatural(0()) -> tt() 1178.87/299.94 , a__isNatural(head(V1)) -> a__isLNat(V1) 1178.87/299.94 , a__isNatural(sel(V1, V2)) -> a__and(a__isNatural(V1), isLNat(V2)) 1178.87/299.94 , a__isLNat(X) -> isLNat(X) 1178.87/299.94 , a__isLNat(cons(V1, V2)) -> a__and(a__isNatural(V1), isLNat(V2)) 1178.87/299.94 , a__isLNat(natsFrom(V1)) -> a__isNatural(V1) 1178.87/299.94 , a__isLNat(nil()) -> tt() 1178.87/299.94 , a__isLNat(afterNth(V1, V2)) -> 1178.87/299.94 a__and(a__isNatural(V1), isLNat(V2)) 1178.87/299.94 , a__isLNat(fst(V1)) -> a__isPLNat(V1) 1178.87/299.94 , a__isLNat(snd(V1)) -> a__isPLNat(V1) 1178.87/299.94 , a__isLNat(tail(V1)) -> a__isLNat(V1) 1178.87/299.94 , a__isLNat(take(V1, V2)) -> a__and(a__isNatural(V1), isLNat(V2)) 1178.87/299.94 , a__isPLNat(X) -> isPLNat(X) 1178.87/299.94 , a__isPLNat(pair(V1, V2)) -> a__and(a__isLNat(V1), isLNat(V2)) 1178.87/299.94 , a__isPLNat(splitAt(V1, V2)) -> 1178.87/299.94 a__and(a__isNatural(V1), isLNat(V2)) 1178.87/299.94 , a__natsFrom(N) -> a__U41(a__isNatural(N), N) 1178.87/299.94 , a__natsFrom(X) -> natsFrom(X) 1178.87/299.94 , a__sel(N, XS) -> 1178.87/299.94 a__U51(a__and(a__isNatural(N), isLNat(XS)), N, XS) 1178.87/299.94 , a__sel(X1, X2) -> sel(X1, X2) 1178.87/299.94 , a__tail(X) -> tail(X) 1178.87/299.94 , a__tail(cons(N, XS)) -> 1178.87/299.94 a__U91(a__and(a__isNatural(N), isLNat(XS)), XS) 1178.87/299.94 , a__take(N, XS) -> 1178.87/299.94 a__U101(a__and(a__isNatural(N), isLNat(XS)), N, XS) 1178.87/299.94 , a__take(X1, X2) -> take(X1, X2) } 1178.87/299.94 Weak DPs: 1178.87/299.94 { mark^#(tt()) -> c_8() 1178.87/299.94 , mark^#(nil()) -> c_13() 1178.87/299.94 , mark^#(0()) -> c_20() 1178.87/299.94 , a__isLNat^#(nil()) -> c_74() 1178.87/299.94 , a__isNatural^#(0()) -> c_68() } 1178.87/299.94 Obligation: 1178.87/299.94 runtime complexity 1178.87/299.94 Answer: 1178.87/299.94 MAYBE 1178.87/299.94 1178.87/299.94 Empty strict component of the problem is NOT empty. 1178.87/299.94 1178.87/299.94 1178.87/299.94 Arrrr.. 1179.10/300.60 EOF