MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { active(pairNs()) -> mark(cons(0(), incr(oddNs())))
  , active(cons(X1, X2)) -> cons(active(X1), X2)
  , active(incr(X)) -> incr(active(X))
  , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS)))
  , active(oddNs()) -> mark(incr(pairNs()))
  , active(s(X)) -> s(active(X))
  , active(take(X1, X2)) -> take(X1, active(X2))
  , active(take(X1, X2)) -> take(active(X1), X2)
  , active(take(0(), XS)) -> mark(nil())
  , active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS)))
  , active(zip(X1, X2)) -> zip(X1, active(X2))
  , active(zip(X1, X2)) -> zip(active(X1), X2)
  , active(zip(X, nil())) -> mark(nil())
  , active(zip(cons(X, XS), cons(Y, YS))) ->
    mark(cons(pair(X, Y), zip(XS, YS)))
  , active(zip(nil(), XS)) -> mark(nil())
  , active(pair(X1, X2)) -> pair(X1, active(X2))
  , active(pair(X1, X2)) -> pair(active(X1), X2)
  , active(tail(X)) -> tail(active(X))
  , active(tail(cons(X, XS))) -> mark(XS)
  , active(repItems(X)) -> repItems(active(X))
  , active(repItems(cons(X, XS))) ->
    mark(cons(X, cons(X, repItems(XS))))
  , active(repItems(nil())) -> mark(nil())
  , cons(mark(X1), X2) -> mark(cons(X1, X2))
  , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
  , incr(mark(X)) -> mark(incr(X))
  , incr(ok(X)) -> ok(incr(X))
  , s(mark(X)) -> mark(s(X))
  , s(ok(X)) -> ok(s(X))
  , take(X1, mark(X2)) -> mark(take(X1, X2))
  , take(mark(X1), X2) -> mark(take(X1, X2))
  , take(ok(X1), ok(X2)) -> ok(take(X1, X2))
  , zip(X1, mark(X2)) -> mark(zip(X1, X2))
  , zip(mark(X1), X2) -> mark(zip(X1, X2))
  , zip(ok(X1), ok(X2)) -> ok(zip(X1, X2))
  , pair(X1, mark(X2)) -> mark(pair(X1, X2))
  , pair(mark(X1), X2) -> mark(pair(X1, X2))
  , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2))
  , tail(mark(X)) -> mark(tail(X))
  , tail(ok(X)) -> ok(tail(X))
  , repItems(mark(X)) -> mark(repItems(X))
  , repItems(ok(X)) -> ok(repItems(X))
  , proper(pairNs()) -> ok(pairNs())
  , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
  , proper(0()) -> ok(0())
  , proper(incr(X)) -> incr(proper(X))
  , proper(oddNs()) -> ok(oddNs())
  , proper(s(X)) -> s(proper(X))
  , proper(take(X1, X2)) -> take(proper(X1), proper(X2))
  , proper(nil()) -> ok(nil())
  , proper(zip(X1, X2)) -> zip(proper(X1), proper(X2))
  , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2))
  , proper(tail(X)) -> tail(proper(X))
  , proper(repItems(X)) -> repItems(proper(X))
  , top(mark(X)) -> top(proper(X))
  , top(ok(X)) -> top(active(X)) }
Obligation:
  runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
   following reason:
   
   Computation stopped due to timeout after 60.0 seconds.

2) 'Best' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
      failed due to the following reason:
      
      Computation stopped due to timeout after 30.0 seconds.
   
   2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
      due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'Bounds with perSymbol-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
      2) 'Bounds with minimal-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
   
   3) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
         to the following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
      2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
         following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
   

3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
   due to the following reason:
   
   We add the following weak dependency pairs:
   
   Strict DPs:
     { active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs())))
     , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
     , active^#(incr(X)) -> c_3(incr^#(active(X)))
     , active^#(incr(cons(X, XS))) -> c_4(cons^#(s(X), incr(XS)))
     , active^#(oddNs()) -> c_5(incr^#(pairNs()))
     , active^#(s(X)) -> c_6(s^#(active(X)))
     , active^#(take(X1, X2)) -> c_7(take^#(X1, active(X2)))
     , active^#(take(X1, X2)) -> c_8(take^#(active(X1), X2))
     , active^#(take(0(), XS)) -> c_9()
     , active^#(take(s(N), cons(X, XS))) -> c_10(cons^#(X, take(N, XS)))
     , active^#(zip(X1, X2)) -> c_11(zip^#(X1, active(X2)))
     , active^#(zip(X1, X2)) -> c_12(zip^#(active(X1), X2))
     , active^#(zip(X, nil())) -> c_13()
     , active^#(zip(cons(X, XS), cons(Y, YS))) ->
       c_14(cons^#(pair(X, Y), zip(XS, YS)))
     , active^#(zip(nil(), XS)) -> c_15()
     , active^#(pair(X1, X2)) -> c_16(pair^#(X1, active(X2)))
     , active^#(pair(X1, X2)) -> c_17(pair^#(active(X1), X2))
     , active^#(tail(X)) -> c_18(tail^#(active(X)))
     , active^#(tail(cons(X, XS))) -> c_19(XS)
     , active^#(repItems(X)) -> c_20(repItems^#(active(X)))
     , active^#(repItems(cons(X, XS))) ->
       c_21(cons^#(X, cons(X, repItems(XS))))
     , active^#(repItems(nil())) -> c_22()
     , cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2))
     , cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2))
     , incr^#(mark(X)) -> c_25(incr^#(X))
     , incr^#(ok(X)) -> c_26(incr^#(X))
     , s^#(mark(X)) -> c_27(s^#(X))
     , s^#(ok(X)) -> c_28(s^#(X))
     , take^#(X1, mark(X2)) -> c_29(take^#(X1, X2))
     , take^#(mark(X1), X2) -> c_30(take^#(X1, X2))
     , take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2))
     , zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2))
     , zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2))
     , zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2))
     , pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2))
     , pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2))
     , pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2))
     , tail^#(mark(X)) -> c_38(tail^#(X))
     , tail^#(ok(X)) -> c_39(tail^#(X))
     , repItems^#(mark(X)) -> c_40(repItems^#(X))
     , repItems^#(ok(X)) -> c_41(repItems^#(X))
     , proper^#(pairNs()) -> c_42()
     , proper^#(cons(X1, X2)) -> c_43(cons^#(proper(X1), proper(X2)))
     , proper^#(0()) -> c_44()
     , proper^#(incr(X)) -> c_45(incr^#(proper(X)))
     , proper^#(oddNs()) -> c_46()
     , proper^#(s(X)) -> c_47(s^#(proper(X)))
     , proper^#(take(X1, X2)) -> c_48(take^#(proper(X1), proper(X2)))
     , proper^#(nil()) -> c_49()
     , proper^#(zip(X1, X2)) -> c_50(zip^#(proper(X1), proper(X2)))
     , proper^#(pair(X1, X2)) -> c_51(pair^#(proper(X1), proper(X2)))
     , proper^#(tail(X)) -> c_52(tail^#(proper(X)))
     , proper^#(repItems(X)) -> c_53(repItems^#(proper(X)))
     , top^#(mark(X)) -> c_54(top^#(proper(X)))
     , top^#(ok(X)) -> c_55(top^#(active(X))) }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs())))
     , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
     , active^#(incr(X)) -> c_3(incr^#(active(X)))
     , active^#(incr(cons(X, XS))) -> c_4(cons^#(s(X), incr(XS)))
     , active^#(oddNs()) -> c_5(incr^#(pairNs()))
     , active^#(s(X)) -> c_6(s^#(active(X)))
     , active^#(take(X1, X2)) -> c_7(take^#(X1, active(X2)))
     , active^#(take(X1, X2)) -> c_8(take^#(active(X1), X2))
     , active^#(take(0(), XS)) -> c_9()
     , active^#(take(s(N), cons(X, XS))) -> c_10(cons^#(X, take(N, XS)))
     , active^#(zip(X1, X2)) -> c_11(zip^#(X1, active(X2)))
     , active^#(zip(X1, X2)) -> c_12(zip^#(active(X1), X2))
     , active^#(zip(X, nil())) -> c_13()
     , active^#(zip(cons(X, XS), cons(Y, YS))) ->
       c_14(cons^#(pair(X, Y), zip(XS, YS)))
     , active^#(zip(nil(), XS)) -> c_15()
     , active^#(pair(X1, X2)) -> c_16(pair^#(X1, active(X2)))
     , active^#(pair(X1, X2)) -> c_17(pair^#(active(X1), X2))
     , active^#(tail(X)) -> c_18(tail^#(active(X)))
     , active^#(tail(cons(X, XS))) -> c_19(XS)
     , active^#(repItems(X)) -> c_20(repItems^#(active(X)))
     , active^#(repItems(cons(X, XS))) ->
       c_21(cons^#(X, cons(X, repItems(XS))))
     , active^#(repItems(nil())) -> c_22()
     , cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2))
     , cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2))
     , incr^#(mark(X)) -> c_25(incr^#(X))
     , incr^#(ok(X)) -> c_26(incr^#(X))
     , s^#(mark(X)) -> c_27(s^#(X))
     , s^#(ok(X)) -> c_28(s^#(X))
     , take^#(X1, mark(X2)) -> c_29(take^#(X1, X2))
     , take^#(mark(X1), X2) -> c_30(take^#(X1, X2))
     , take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2))
     , zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2))
     , zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2))
     , zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2))
     , pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2))
     , pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2))
     , pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2))
     , tail^#(mark(X)) -> c_38(tail^#(X))
     , tail^#(ok(X)) -> c_39(tail^#(X))
     , repItems^#(mark(X)) -> c_40(repItems^#(X))
     , repItems^#(ok(X)) -> c_41(repItems^#(X))
     , proper^#(pairNs()) -> c_42()
     , proper^#(cons(X1, X2)) -> c_43(cons^#(proper(X1), proper(X2)))
     , proper^#(0()) -> c_44()
     , proper^#(incr(X)) -> c_45(incr^#(proper(X)))
     , proper^#(oddNs()) -> c_46()
     , proper^#(s(X)) -> c_47(s^#(proper(X)))
     , proper^#(take(X1, X2)) -> c_48(take^#(proper(X1), proper(X2)))
     , proper^#(nil()) -> c_49()
     , proper^#(zip(X1, X2)) -> c_50(zip^#(proper(X1), proper(X2)))
     , proper^#(pair(X1, X2)) -> c_51(pair^#(proper(X1), proper(X2)))
     , proper^#(tail(X)) -> c_52(tail^#(proper(X)))
     , proper^#(repItems(X)) -> c_53(repItems^#(proper(X)))
     , top^#(mark(X)) -> c_54(top^#(proper(X)))
     , top^#(ok(X)) -> c_55(top^#(active(X))) }
   Strict Trs:
     { active(pairNs()) -> mark(cons(0(), incr(oddNs())))
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(incr(X)) -> incr(active(X))
     , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS)))
     , active(oddNs()) -> mark(incr(pairNs()))
     , active(s(X)) -> s(active(X))
     , active(take(X1, X2)) -> take(X1, active(X2))
     , active(take(X1, X2)) -> take(active(X1), X2)
     , active(take(0(), XS)) -> mark(nil())
     , active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS)))
     , active(zip(X1, X2)) -> zip(X1, active(X2))
     , active(zip(X1, X2)) -> zip(active(X1), X2)
     , active(zip(X, nil())) -> mark(nil())
     , active(zip(cons(X, XS), cons(Y, YS))) ->
       mark(cons(pair(X, Y), zip(XS, YS)))
     , active(zip(nil(), XS)) -> mark(nil())
     , active(pair(X1, X2)) -> pair(X1, active(X2))
     , active(pair(X1, X2)) -> pair(active(X1), X2)
     , active(tail(X)) -> tail(active(X))
     , active(tail(cons(X, XS))) -> mark(XS)
     , active(repItems(X)) -> repItems(active(X))
     , active(repItems(cons(X, XS))) ->
       mark(cons(X, cons(X, repItems(XS))))
     , active(repItems(nil())) -> mark(nil())
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , incr(mark(X)) -> mark(incr(X))
     , incr(ok(X)) -> ok(incr(X))
     , s(mark(X)) -> mark(s(X))
     , s(ok(X)) -> ok(s(X))
     , take(X1, mark(X2)) -> mark(take(X1, X2))
     , take(mark(X1), X2) -> mark(take(X1, X2))
     , take(ok(X1), ok(X2)) -> ok(take(X1, X2))
     , zip(X1, mark(X2)) -> mark(zip(X1, X2))
     , zip(mark(X1), X2) -> mark(zip(X1, X2))
     , zip(ok(X1), ok(X2)) -> ok(zip(X1, X2))
     , pair(X1, mark(X2)) -> mark(pair(X1, X2))
     , pair(mark(X1), X2) -> mark(pair(X1, X2))
     , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2))
     , tail(mark(X)) -> mark(tail(X))
     , tail(ok(X)) -> ok(tail(X))
     , repItems(mark(X)) -> mark(repItems(X))
     , repItems(ok(X)) -> ok(repItems(X))
     , proper(pairNs()) -> ok(pairNs())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(incr(X)) -> incr(proper(X))
     , proper(oddNs()) -> ok(oddNs())
     , proper(s(X)) -> s(proper(X))
     , proper(take(X1, X2)) -> take(proper(X1), proper(X2))
     , proper(nil()) -> ok(nil())
     , proper(zip(X1, X2)) -> zip(proper(X1), proper(X2))
     , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2))
     , proper(tail(X)) -> tail(proper(X))
     , proper(repItems(X)) -> repItems(proper(X))
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(X)) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Consider the dependency graph:
   
     1: active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs())))
     
     2: active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
        -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24
        -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23
     
     3: active^#(incr(X)) -> c_3(incr^#(active(X)))
        -->_1 incr^#(ok(X)) -> c_26(incr^#(X)) :26
        -->_1 incr^#(mark(X)) -> c_25(incr^#(X)) :25
     
     4: active^#(incr(cons(X, XS))) -> c_4(cons^#(s(X), incr(XS)))
        -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24
        -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23
     
     5: active^#(oddNs()) -> c_5(incr^#(pairNs()))
     
     6: active^#(s(X)) -> c_6(s^#(active(X)))
        -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28
        -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27
     
     7: active^#(take(X1, X2)) -> c_7(take^#(X1, active(X2)))
        -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31
        -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30
        -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29
     
     8: active^#(take(X1, X2)) -> c_8(take^#(active(X1), X2))
        -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31
        -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30
        -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29
     
     9: active^#(take(0(), XS)) -> c_9()
     
     10: active^#(take(s(N), cons(X, XS))) ->
         c_10(cons^#(X, take(N, XS)))
        -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24
        -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23
     
     11: active^#(zip(X1, X2)) -> c_11(zip^#(X1, active(X2)))
        -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34
        -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33
        -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32
     
     12: active^#(zip(X1, X2)) -> c_12(zip^#(active(X1), X2))
        -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34
        -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33
        -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32
     
     13: active^#(zip(X, nil())) -> c_13()
     
     14: active^#(zip(cons(X, XS), cons(Y, YS))) ->
         c_14(cons^#(pair(X, Y), zip(XS, YS)))
        -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24
        -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23
     
     15: active^#(zip(nil(), XS)) -> c_15()
     
     16: active^#(pair(X1, X2)) -> c_16(pair^#(X1, active(X2)))
        -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37
        -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36
        -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35
     
     17: active^#(pair(X1, X2)) -> c_17(pair^#(active(X1), X2))
        -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37
        -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36
        -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35
     
     18: active^#(tail(X)) -> c_18(tail^#(active(X)))
        -->_1 tail^#(ok(X)) -> c_39(tail^#(X)) :39
        -->_1 tail^#(mark(X)) -> c_38(tail^#(X)) :38
     
     19: active^#(tail(cons(X, XS))) -> c_19(XS)
        -->_1 top^#(ok(X)) -> c_55(top^#(active(X))) :55
        -->_1 top^#(mark(X)) -> c_54(top^#(proper(X))) :54
        -->_1 proper^#(repItems(X)) -> c_53(repItems^#(proper(X))) :53
        -->_1 proper^#(tail(X)) -> c_52(tail^#(proper(X))) :52
        -->_1 proper^#(pair(X1, X2)) ->
              c_51(pair^#(proper(X1), proper(X2))) :51
        -->_1 proper^#(zip(X1, X2)) ->
              c_50(zip^#(proper(X1), proper(X2))) :50
        -->_1 proper^#(take(X1, X2)) ->
              c_48(take^#(proper(X1), proper(X2))) :48
        -->_1 proper^#(s(X)) -> c_47(s^#(proper(X))) :47
        -->_1 proper^#(incr(X)) -> c_45(incr^#(proper(X))) :45
        -->_1 proper^#(cons(X1, X2)) ->
              c_43(cons^#(proper(X1), proper(X2))) :43
        -->_1 repItems^#(ok(X)) -> c_41(repItems^#(X)) :41
        -->_1 repItems^#(mark(X)) -> c_40(repItems^#(X)) :40
        -->_1 tail^#(ok(X)) -> c_39(tail^#(X)) :39
        -->_1 tail^#(mark(X)) -> c_38(tail^#(X)) :38
        -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37
        -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36
        -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35
        -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34
        -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33
        -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32
        -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31
        -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30
        -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29
        -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28
        -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27
        -->_1 incr^#(ok(X)) -> c_26(incr^#(X)) :26
        -->_1 incr^#(mark(X)) -> c_25(incr^#(X)) :25
        -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24
        -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23
        -->_1 active^#(repItems(cons(X, XS))) ->
              c_21(cons^#(X, cons(X, repItems(XS)))) :21
        -->_1 active^#(repItems(X)) -> c_20(repItems^#(active(X))) :20
        -->_1 proper^#(nil()) -> c_49() :49
        -->_1 proper^#(oddNs()) -> c_46() :46
        -->_1 proper^#(0()) -> c_44() :44
        -->_1 proper^#(pairNs()) -> c_42() :42
        -->_1 active^#(repItems(nil())) -> c_22() :22
        -->_1 active^#(tail(cons(X, XS))) -> c_19(XS) :19
        -->_1 active^#(tail(X)) -> c_18(tail^#(active(X))) :18
        -->_1 active^#(pair(X1, X2)) -> c_17(pair^#(active(X1), X2)) :17
        -->_1 active^#(pair(X1, X2)) -> c_16(pair^#(X1, active(X2))) :16
        -->_1 active^#(zip(nil(), XS)) -> c_15() :15
        -->_1 active^#(zip(cons(X, XS), cons(Y, YS))) ->
              c_14(cons^#(pair(X, Y), zip(XS, YS))) :14
        -->_1 active^#(zip(X, nil())) -> c_13() :13
        -->_1 active^#(zip(X1, X2)) -> c_12(zip^#(active(X1), X2)) :12
        -->_1 active^#(zip(X1, X2)) -> c_11(zip^#(X1, active(X2))) :11
        -->_1 active^#(take(s(N), cons(X, XS))) ->
              c_10(cons^#(X, take(N, XS))) :10
        -->_1 active^#(take(0(), XS)) -> c_9() :9
        -->_1 active^#(take(X1, X2)) -> c_8(take^#(active(X1), X2)) :8
        -->_1 active^#(take(X1, X2)) -> c_7(take^#(X1, active(X2))) :7
        -->_1 active^#(s(X)) -> c_6(s^#(active(X))) :6
        -->_1 active^#(oddNs()) -> c_5(incr^#(pairNs())) :5
        -->_1 active^#(incr(cons(X, XS))) -> c_4(cons^#(s(X), incr(XS))) :4
        -->_1 active^#(incr(X)) -> c_3(incr^#(active(X))) :3
        -->_1 active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) :2
        -->_1 active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs()))) :1
     
     20: active^#(repItems(X)) -> c_20(repItems^#(active(X)))
        -->_1 repItems^#(ok(X)) -> c_41(repItems^#(X)) :41
        -->_1 repItems^#(mark(X)) -> c_40(repItems^#(X)) :40
     
     21: active^#(repItems(cons(X, XS))) ->
         c_21(cons^#(X, cons(X, repItems(XS))))
        -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24
        -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23
     
     22: active^#(repItems(nil())) -> c_22()
     
     23: cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2))
        -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24
        -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23
     
     24: cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2))
        -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24
        -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23
     
     25: incr^#(mark(X)) -> c_25(incr^#(X))
        -->_1 incr^#(ok(X)) -> c_26(incr^#(X)) :26
        -->_1 incr^#(mark(X)) -> c_25(incr^#(X)) :25
     
     26: incr^#(ok(X)) -> c_26(incr^#(X))
        -->_1 incr^#(ok(X)) -> c_26(incr^#(X)) :26
        -->_1 incr^#(mark(X)) -> c_25(incr^#(X)) :25
     
     27: s^#(mark(X)) -> c_27(s^#(X))
        -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28
        -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27
     
     28: s^#(ok(X)) -> c_28(s^#(X))
        -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28
        -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27
     
     29: take^#(X1, mark(X2)) -> c_29(take^#(X1, X2))
        -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31
        -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30
        -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29
     
     30: take^#(mark(X1), X2) -> c_30(take^#(X1, X2))
        -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31
        -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30
        -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29
     
     31: take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2))
        -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31
        -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30
        -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29
     
     32: zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2))
        -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34
        -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33
        -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32
     
     33: zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2))
        -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34
        -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33
        -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32
     
     34: zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2))
        -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34
        -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33
        -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32
     
     35: pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2))
        -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37
        -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36
        -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35
     
     36: pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2))
        -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37
        -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36
        -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35
     
     37: pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2))
        -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37
        -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36
        -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35
     
     38: tail^#(mark(X)) -> c_38(tail^#(X))
        -->_1 tail^#(ok(X)) -> c_39(tail^#(X)) :39
        -->_1 tail^#(mark(X)) -> c_38(tail^#(X)) :38
     
     39: tail^#(ok(X)) -> c_39(tail^#(X))
        -->_1 tail^#(ok(X)) -> c_39(tail^#(X)) :39
        -->_1 tail^#(mark(X)) -> c_38(tail^#(X)) :38
     
     40: repItems^#(mark(X)) -> c_40(repItems^#(X))
        -->_1 repItems^#(ok(X)) -> c_41(repItems^#(X)) :41
        -->_1 repItems^#(mark(X)) -> c_40(repItems^#(X)) :40
     
     41: repItems^#(ok(X)) -> c_41(repItems^#(X))
        -->_1 repItems^#(ok(X)) -> c_41(repItems^#(X)) :41
        -->_1 repItems^#(mark(X)) -> c_40(repItems^#(X)) :40
     
     42: proper^#(pairNs()) -> c_42()
     
     43: proper^#(cons(X1, X2)) -> c_43(cons^#(proper(X1), proper(X2)))
        -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24
        -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23
     
     44: proper^#(0()) -> c_44()
     
     45: proper^#(incr(X)) -> c_45(incr^#(proper(X)))
        -->_1 incr^#(ok(X)) -> c_26(incr^#(X)) :26
        -->_1 incr^#(mark(X)) -> c_25(incr^#(X)) :25
     
     46: proper^#(oddNs()) -> c_46()
     
     47: proper^#(s(X)) -> c_47(s^#(proper(X)))
        -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28
        -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27
     
     48: proper^#(take(X1, X2)) -> c_48(take^#(proper(X1), proper(X2)))
        -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31
        -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30
        -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29
     
     49: proper^#(nil()) -> c_49()
     
     50: proper^#(zip(X1, X2)) -> c_50(zip^#(proper(X1), proper(X2)))
        -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34
        -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33
        -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32
     
     51: proper^#(pair(X1, X2)) -> c_51(pair^#(proper(X1), proper(X2)))
        -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37
        -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36
        -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35
     
     52: proper^#(tail(X)) -> c_52(tail^#(proper(X)))
        -->_1 tail^#(ok(X)) -> c_39(tail^#(X)) :39
        -->_1 tail^#(mark(X)) -> c_38(tail^#(X)) :38
     
     53: proper^#(repItems(X)) -> c_53(repItems^#(proper(X)))
        -->_1 repItems^#(ok(X)) -> c_41(repItems^#(X)) :41
        -->_1 repItems^#(mark(X)) -> c_40(repItems^#(X)) :40
     
     54: top^#(mark(X)) -> c_54(top^#(proper(X)))
        -->_1 top^#(ok(X)) -> c_55(top^#(active(X))) :55
        -->_1 top^#(mark(X)) -> c_54(top^#(proper(X))) :54
     
     55: top^#(ok(X)) -> c_55(top^#(active(X)))
        -->_1 top^#(ok(X)) -> c_55(top^#(active(X))) :55
        -->_1 top^#(mark(X)) -> c_54(top^#(proper(X))) :54
     
   
   Only the nodes
   {1,5,23,24,25,26,27,28,29,31,30,32,34,33,35,37,36,38,39,40,41,42,44,46,49,54,55}
   are reachable from nodes
   {1,5,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,44,46,49,54,55}
   that start derivation from marked basic terms. The nodes not
   reachable are removed from the problem.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs())))
     , active^#(oddNs()) -> c_5(incr^#(pairNs()))
     , cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2))
     , cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2))
     , incr^#(mark(X)) -> c_25(incr^#(X))
     , incr^#(ok(X)) -> c_26(incr^#(X))
     , s^#(mark(X)) -> c_27(s^#(X))
     , s^#(ok(X)) -> c_28(s^#(X))
     , take^#(X1, mark(X2)) -> c_29(take^#(X1, X2))
     , take^#(mark(X1), X2) -> c_30(take^#(X1, X2))
     , take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2))
     , zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2))
     , zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2))
     , zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2))
     , pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2))
     , pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2))
     , pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2))
     , tail^#(mark(X)) -> c_38(tail^#(X))
     , tail^#(ok(X)) -> c_39(tail^#(X))
     , repItems^#(mark(X)) -> c_40(repItems^#(X))
     , repItems^#(ok(X)) -> c_41(repItems^#(X))
     , proper^#(pairNs()) -> c_42()
     , proper^#(0()) -> c_44()
     , proper^#(oddNs()) -> c_46()
     , proper^#(nil()) -> c_49()
     , top^#(mark(X)) -> c_54(top^#(proper(X)))
     , top^#(ok(X)) -> c_55(top^#(active(X))) }
   Strict Trs:
     { active(pairNs()) -> mark(cons(0(), incr(oddNs())))
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(incr(X)) -> incr(active(X))
     , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS)))
     , active(oddNs()) -> mark(incr(pairNs()))
     , active(s(X)) -> s(active(X))
     , active(take(X1, X2)) -> take(X1, active(X2))
     , active(take(X1, X2)) -> take(active(X1), X2)
     , active(take(0(), XS)) -> mark(nil())
     , active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS)))
     , active(zip(X1, X2)) -> zip(X1, active(X2))
     , active(zip(X1, X2)) -> zip(active(X1), X2)
     , active(zip(X, nil())) -> mark(nil())
     , active(zip(cons(X, XS), cons(Y, YS))) ->
       mark(cons(pair(X, Y), zip(XS, YS)))
     , active(zip(nil(), XS)) -> mark(nil())
     , active(pair(X1, X2)) -> pair(X1, active(X2))
     , active(pair(X1, X2)) -> pair(active(X1), X2)
     , active(tail(X)) -> tail(active(X))
     , active(tail(cons(X, XS))) -> mark(XS)
     , active(repItems(X)) -> repItems(active(X))
     , active(repItems(cons(X, XS))) ->
       mark(cons(X, cons(X, repItems(XS))))
     , active(repItems(nil())) -> mark(nil())
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , incr(mark(X)) -> mark(incr(X))
     , incr(ok(X)) -> ok(incr(X))
     , s(mark(X)) -> mark(s(X))
     , s(ok(X)) -> ok(s(X))
     , take(X1, mark(X2)) -> mark(take(X1, X2))
     , take(mark(X1), X2) -> mark(take(X1, X2))
     , take(ok(X1), ok(X2)) -> ok(take(X1, X2))
     , zip(X1, mark(X2)) -> mark(zip(X1, X2))
     , zip(mark(X1), X2) -> mark(zip(X1, X2))
     , zip(ok(X1), ok(X2)) -> ok(zip(X1, X2))
     , pair(X1, mark(X2)) -> mark(pair(X1, X2))
     , pair(mark(X1), X2) -> mark(pair(X1, X2))
     , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2))
     , tail(mark(X)) -> mark(tail(X))
     , tail(ok(X)) -> ok(tail(X))
     , repItems(mark(X)) -> mark(repItems(X))
     , repItems(ok(X)) -> ok(repItems(X))
     , proper(pairNs()) -> ok(pairNs())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(incr(X)) -> incr(proper(X))
     , proper(oddNs()) -> ok(oddNs())
     , proper(s(X)) -> s(proper(X))
     , proper(take(X1, X2)) -> take(proper(X1), proper(X2))
     , proper(nil()) -> ok(nil())
     , proper(zip(X1, X2)) -> zip(proper(X1), proper(X2))
     , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2))
     , proper(tail(X)) -> tail(proper(X))
     , proper(repItems(X)) -> repItems(proper(X))
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(X)) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {1,2,22,23,24,25} by
   applications of Pre({1,2,22,23,24,25}) = {}. Here rules are labeled
   as follows:
   
     DPs:
       { 1: active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs())))
       , 2: active^#(oddNs()) -> c_5(incr^#(pairNs()))
       , 3: cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2))
       , 4: cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2))
       , 5: incr^#(mark(X)) -> c_25(incr^#(X))
       , 6: incr^#(ok(X)) -> c_26(incr^#(X))
       , 7: s^#(mark(X)) -> c_27(s^#(X))
       , 8: s^#(ok(X)) -> c_28(s^#(X))
       , 9: take^#(X1, mark(X2)) -> c_29(take^#(X1, X2))
       , 10: take^#(mark(X1), X2) -> c_30(take^#(X1, X2))
       , 11: take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2))
       , 12: zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2))
       , 13: zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2))
       , 14: zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2))
       , 15: pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2))
       , 16: pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2))
       , 17: pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2))
       , 18: tail^#(mark(X)) -> c_38(tail^#(X))
       , 19: tail^#(ok(X)) -> c_39(tail^#(X))
       , 20: repItems^#(mark(X)) -> c_40(repItems^#(X))
       , 21: repItems^#(ok(X)) -> c_41(repItems^#(X))
       , 22: proper^#(pairNs()) -> c_42()
       , 23: proper^#(0()) -> c_44()
       , 24: proper^#(oddNs()) -> c_46()
       , 25: proper^#(nil()) -> c_49()
       , 26: top^#(mark(X)) -> c_54(top^#(proper(X)))
       , 27: top^#(ok(X)) -> c_55(top^#(active(X))) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2))
     , cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2))
     , incr^#(mark(X)) -> c_25(incr^#(X))
     , incr^#(ok(X)) -> c_26(incr^#(X))
     , s^#(mark(X)) -> c_27(s^#(X))
     , s^#(ok(X)) -> c_28(s^#(X))
     , take^#(X1, mark(X2)) -> c_29(take^#(X1, X2))
     , take^#(mark(X1), X2) -> c_30(take^#(X1, X2))
     , take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2))
     , zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2))
     , zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2))
     , zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2))
     , pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2))
     , pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2))
     , pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2))
     , tail^#(mark(X)) -> c_38(tail^#(X))
     , tail^#(ok(X)) -> c_39(tail^#(X))
     , repItems^#(mark(X)) -> c_40(repItems^#(X))
     , repItems^#(ok(X)) -> c_41(repItems^#(X))
     , top^#(mark(X)) -> c_54(top^#(proper(X)))
     , top^#(ok(X)) -> c_55(top^#(active(X))) }
   Strict Trs:
     { active(pairNs()) -> mark(cons(0(), incr(oddNs())))
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(incr(X)) -> incr(active(X))
     , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS)))
     , active(oddNs()) -> mark(incr(pairNs()))
     , active(s(X)) -> s(active(X))
     , active(take(X1, X2)) -> take(X1, active(X2))
     , active(take(X1, X2)) -> take(active(X1), X2)
     , active(take(0(), XS)) -> mark(nil())
     , active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS)))
     , active(zip(X1, X2)) -> zip(X1, active(X2))
     , active(zip(X1, X2)) -> zip(active(X1), X2)
     , active(zip(X, nil())) -> mark(nil())
     , active(zip(cons(X, XS), cons(Y, YS))) ->
       mark(cons(pair(X, Y), zip(XS, YS)))
     , active(zip(nil(), XS)) -> mark(nil())
     , active(pair(X1, X2)) -> pair(X1, active(X2))
     , active(pair(X1, X2)) -> pair(active(X1), X2)
     , active(tail(X)) -> tail(active(X))
     , active(tail(cons(X, XS))) -> mark(XS)
     , active(repItems(X)) -> repItems(active(X))
     , active(repItems(cons(X, XS))) ->
       mark(cons(X, cons(X, repItems(XS))))
     , active(repItems(nil())) -> mark(nil())
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , incr(mark(X)) -> mark(incr(X))
     , incr(ok(X)) -> ok(incr(X))
     , s(mark(X)) -> mark(s(X))
     , s(ok(X)) -> ok(s(X))
     , take(X1, mark(X2)) -> mark(take(X1, X2))
     , take(mark(X1), X2) -> mark(take(X1, X2))
     , take(ok(X1), ok(X2)) -> ok(take(X1, X2))
     , zip(X1, mark(X2)) -> mark(zip(X1, X2))
     , zip(mark(X1), X2) -> mark(zip(X1, X2))
     , zip(ok(X1), ok(X2)) -> ok(zip(X1, X2))
     , pair(X1, mark(X2)) -> mark(pair(X1, X2))
     , pair(mark(X1), X2) -> mark(pair(X1, X2))
     , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2))
     , tail(mark(X)) -> mark(tail(X))
     , tail(ok(X)) -> ok(tail(X))
     , repItems(mark(X)) -> mark(repItems(X))
     , repItems(ok(X)) -> ok(repItems(X))
     , proper(pairNs()) -> ok(pairNs())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(incr(X)) -> incr(proper(X))
     , proper(oddNs()) -> ok(oddNs())
     , proper(s(X)) -> s(proper(X))
     , proper(take(X1, X2)) -> take(proper(X1), proper(X2))
     , proper(nil()) -> ok(nil())
     , proper(zip(X1, X2)) -> zip(proper(X1), proper(X2))
     , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2))
     , proper(tail(X)) -> tail(proper(X))
     , proper(repItems(X)) -> repItems(proper(X))
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(X)) }
   Weak DPs:
     { active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs())))
     , active^#(oddNs()) -> c_5(incr^#(pairNs()))
     , proper^#(pairNs()) -> c_42()
     , proper^#(0()) -> c_44()
     , proper^#(oddNs()) -> c_46()
     , proper^#(nil()) -> c_49() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..