MAYBE

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

Strict Trs:
  { U11(tt(), N, X, XS) -> U12(splitAt(N, XS), X)
  , U12(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y
  , and(tt(), X) -> X
  , fst(pair(X, Y)) -> X
  , head(cons(N, XS)) -> N
  , natsFrom(N) -> cons(N, natsFrom(s(N)))
  , sel(N, XS) -> head(afterNth(N, XS))
  , tail(cons(N, XS)) -> XS
  , take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following weak dependency pairs:

Strict DPs:
  { U11^#(tt(), N, X, XS) -> c_1(U12^#(splitAt(N, XS), X))
  , U12^#(pair(YS, ZS), X) -> c_2()
  , splitAt^#(s(N), cons(X, XS)) -> c_3(U11^#(tt(), N, X, XS))
  , splitAt^#(0(), XS) -> c_4()
  , afterNth^#(N, XS) -> c_5(snd^#(splitAt(N, XS)))
  , snd^#(pair(X, Y)) -> c_6()
  , and^#(tt(), X) -> c_7()
  , fst^#(pair(X, Y)) -> c_8()
  , head^#(cons(N, XS)) -> c_9()
  , natsFrom^#(N) -> c_10(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_11(head^#(afterNth(N, XS)))
  , tail^#(cons(N, XS)) -> c_12()
  , take^#(N, XS) -> c_13(fst^#(splitAt(N, XS))) }

and mark the set of starting terms.

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

Strict DPs:
  { U11^#(tt(), N, X, XS) -> c_1(U12^#(splitAt(N, XS), X))
  , U12^#(pair(YS, ZS), X) -> c_2()
  , splitAt^#(s(N), cons(X, XS)) -> c_3(U11^#(tt(), N, X, XS))
  , splitAt^#(0(), XS) -> c_4()
  , afterNth^#(N, XS) -> c_5(snd^#(splitAt(N, XS)))
  , snd^#(pair(X, Y)) -> c_6()
  , and^#(tt(), X) -> c_7()
  , fst^#(pair(X, Y)) -> c_8()
  , head^#(cons(N, XS)) -> c_9()
  , natsFrom^#(N) -> c_10(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_11(head^#(afterNth(N, XS)))
  , tail^#(cons(N, XS)) -> c_12()
  , take^#(N, XS) -> c_13(fst^#(splitAt(N, XS))) }
Strict Trs:
  { U11(tt(), N, X, XS) -> U12(splitAt(N, XS), X)
  , U12(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y
  , and(tt(), X) -> X
  , fst(pair(X, Y)) -> X
  , head(cons(N, XS)) -> N
  , natsFrom(N) -> cons(N, natsFrom(s(N)))
  , sel(N, XS) -> head(afterNth(N, XS))
  , tail(cons(N, XS)) -> XS
  , take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Strict Usable Rules:
    { U11(tt(), N, X, XS) -> U12(splitAt(N, XS), X)
    , U12(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
    , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, XS)
    , splitAt(0(), XS) -> pair(nil(), XS)
    , afterNth(N, XS) -> snd(splitAt(N, XS))
    , snd(pair(X, Y)) -> Y }

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

Strict DPs:
  { U11^#(tt(), N, X, XS) -> c_1(U12^#(splitAt(N, XS), X))
  , U12^#(pair(YS, ZS), X) -> c_2()
  , splitAt^#(s(N), cons(X, XS)) -> c_3(U11^#(tt(), N, X, XS))
  , splitAt^#(0(), XS) -> c_4()
  , afterNth^#(N, XS) -> c_5(snd^#(splitAt(N, XS)))
  , snd^#(pair(X, Y)) -> c_6()
  , and^#(tt(), X) -> c_7()
  , fst^#(pair(X, Y)) -> c_8()
  , head^#(cons(N, XS)) -> c_9()
  , natsFrom^#(N) -> c_10(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_11(head^#(afterNth(N, XS)))
  , tail^#(cons(N, XS)) -> c_12()
  , take^#(N, XS) -> c_13(fst^#(splitAt(N, XS))) }
Strict Trs:
  { U11(tt(), N, X, XS) -> U12(splitAt(N, XS), X)
  , U12(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The weightgap principle applies (using the following constant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(U12) = {1}, Uargs(snd) = {1}, Uargs(c_1) = {1},
  Uargs(U12^#) = {1}, Uargs(c_3) = {1}, Uargs(c_5) = {1},
  Uargs(snd^#) = {1}, Uargs(fst^#) = {1}, Uargs(head^#) = {1},
  Uargs(c_10) = {1}, Uargs(c_11) = {1}, Uargs(c_13) = {1}

TcT has computed following constructor-restricted matrix
interpretation.

    [U11](x1, x2, x3, x4) = [1] x1 + [2] x2 + [1] x3 + [1] x4 + [2]
                                                                   
                     [tt] = [1]                                    
                                                                   
            [U12](x1, x2) = [1] x1 + [1] x2 + [1]                  
                                                                   
        [splitAt](x1, x2) = [2] x1 + [1] x2 + [0]                  
                                                                   
           [pair](x1, x2) = [1] x2 + [0]                           
                                                                   
           [cons](x1, x2) = [1] x1 + [1] x2 + [0]                  
                                                                   
       [afterNth](x1, x2) = [2] x1 + [1] x2 + [2]                  
                                                                   
                [snd](x1) = [1] x1 + [1]                           
                                                                   
                  [s](x1) = [1] x1 + [2]                           
                                                                   
                      [0] = [2]                                    
                                                                   
                    [nil] = [2]                                    
                                                                   
  [U11^#](x1, x2, x3, x4) = [2] x1 + [2] x2 + [1] x3 + [1] x4 + [2]
                                                                   
                [c_1](x1) = [1] x1 + [2]                           
                                                                   
          [U12^#](x1, x2) = [1] x1 + [1] x2 + [2]                  
                                                                   
                    [c_2] = [1]                                    
                                                                   
      [splitAt^#](x1, x2) = [2] x1 + [1] x2 + [2]                  
                                                                   
                [c_3](x1) = [1] x1 + [2]                           
                                                                   
                    [c_4] = [1]                                    
                                                                   
     [afterNth^#](x1, x2) = [2] x1 + [1] x2 + [1]                  
                                                                   
                [c_5](x1) = [1] x1 + [2]                           
                                                                   
              [snd^#](x1) = [1] x1 + [2]                           
                                                                   
                    [c_6] = [1]                                    
                                                                   
          [and^#](x1, x2) = [2] x1 + [1]                           
                                                                   
                    [c_7] = [2]                                    
                                                                   
              [fst^#](x1) = [1] x1 + [2]                           
                                                                   
                    [c_8] = [1]                                    
                                                                   
             [head^#](x1) = [1] x1 + [2]                           
                                                                   
                    [c_9] = [1]                                    
                                                                   
         [natsFrom^#](x1) = [1] x1 + [1]                           
                                                                   
               [c_10](x1) = [1] x1 + [1]                           
                                                                   
          [sel^#](x1, x2) = [2] x1 + [2] x2 + [1]                  
                                                                   
               [c_11](x1) = [1] x1 + [2]                           
                                                                   
             [tail^#](x1) = [1] x1 + [2]                           
                                                                   
                   [c_12] = [1]                                    
                                                                   
         [take^#](x1, x2) = [2] x1 + [1] x2 + [1]                  
                                                                   
               [c_13](x1) = [1] x1 + [2]                           

This order satisfies following ordering constraints:

         [U11(tt(), N, X, XS)] = [2] N + [1] X + [1] XS + [3]
                               > [2] N + [1] X + [1] XS + [1]
                               = [U12(splitAt(N, XS), X)]    
                                                             
        [U12(pair(YS, ZS), X)] = [1] X + [1] ZS + [1]        
                               > [1] ZS + [0]                
                               = [pair(cons(X, YS), ZS)]     
                                                             
  [splitAt(s(N), cons(X, XS))] = [2] N + [1] X + [1] XS + [4]
                               > [2] N + [1] X + [1] XS + [3]
                               = [U11(tt(), N, X, XS)]       
                                                             
            [splitAt(0(), XS)] = [1] XS + [4]                
                               > [1] XS + [0]                
                               = [pair(nil(), XS)]           
                                                             
             [afterNth(N, XS)] = [2] N + [1] XS + [2]        
                               > [2] N + [1] XS + [1]        
                               = [snd(splitAt(N, XS))]       
                                                             
             [snd(pair(X, Y))] = [1] Y + [1]                 
                               > [1] Y + [0]                 
                               = [Y]                         
                                                             

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

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

Strict DPs:
  { U11^#(tt(), N, X, XS) -> c_1(U12^#(splitAt(N, XS), X))
  , splitAt^#(s(N), cons(X, XS)) -> c_3(U11^#(tt(), N, X, XS))
  , afterNth^#(N, XS) -> c_5(snd^#(splitAt(N, XS)))
  , natsFrom^#(N) -> c_10(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_11(head^#(afterNth(N, XS)))
  , take^#(N, XS) -> c_13(fst^#(splitAt(N, XS))) }
Weak DPs:
  { U12^#(pair(YS, ZS), X) -> c_2()
  , splitAt^#(0(), XS) -> c_4()
  , snd^#(pair(X, Y)) -> c_6()
  , and^#(tt(), X) -> c_7()
  , fst^#(pair(X, Y)) -> c_8()
  , head^#(cons(N, XS)) -> c_9()
  , tail^#(cons(N, XS)) -> c_12() }
Weak Trs:
  { U11(tt(), N, X, XS) -> U12(splitAt(N, XS), X)
  , U12(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {1,3,5,6} by applications
of Pre({1,3,5,6}) = {2}. Here rules are labeled as follows:

  DPs:
    { 1: U11^#(tt(), N, X, XS) -> c_1(U12^#(splitAt(N, XS), X))
    , 2: splitAt^#(s(N), cons(X, XS)) -> c_3(U11^#(tt(), N, X, XS))
    , 3: afterNth^#(N, XS) -> c_5(snd^#(splitAt(N, XS)))
    , 4: natsFrom^#(N) -> c_10(natsFrom^#(s(N)))
    , 5: sel^#(N, XS) -> c_11(head^#(afterNth(N, XS)))
    , 6: take^#(N, XS) -> c_13(fst^#(splitAt(N, XS)))
    , 7: U12^#(pair(YS, ZS), X) -> c_2()
    , 8: splitAt^#(0(), XS) -> c_4()
    , 9: snd^#(pair(X, Y)) -> c_6()
    , 10: and^#(tt(), X) -> c_7()
    , 11: fst^#(pair(X, Y)) -> c_8()
    , 12: head^#(cons(N, XS)) -> c_9()
    , 13: tail^#(cons(N, XS)) -> c_12() }

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

Strict DPs:
  { splitAt^#(s(N), cons(X, XS)) -> c_3(U11^#(tt(), N, X, XS))
  , natsFrom^#(N) -> c_10(natsFrom^#(s(N))) }
Weak DPs:
  { U11^#(tt(), N, X, XS) -> c_1(U12^#(splitAt(N, XS), X))
  , U12^#(pair(YS, ZS), X) -> c_2()
  , splitAt^#(0(), XS) -> c_4()
  , afterNth^#(N, XS) -> c_5(snd^#(splitAt(N, XS)))
  , snd^#(pair(X, Y)) -> c_6()
  , and^#(tt(), X) -> c_7()
  , fst^#(pair(X, Y)) -> c_8()
  , head^#(cons(N, XS)) -> c_9()
  , sel^#(N, XS) -> c_11(head^#(afterNth(N, XS)))
  , tail^#(cons(N, XS)) -> c_12()
  , take^#(N, XS) -> c_13(fst^#(splitAt(N, XS))) }
Weak Trs:
  { U11(tt(), N, X, XS) -> U12(splitAt(N, XS), X)
  , U12(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {1} by applications of
Pre({1}) = {}. Here rules are labeled as follows:

  DPs:
    { 1: splitAt^#(s(N), cons(X, XS)) -> c_3(U11^#(tt(), N, X, XS))
    , 2: natsFrom^#(N) -> c_10(natsFrom^#(s(N)))
    , 3: U11^#(tt(), N, X, XS) -> c_1(U12^#(splitAt(N, XS), X))
    , 4: U12^#(pair(YS, ZS), X) -> c_2()
    , 5: splitAt^#(0(), XS) -> c_4()
    , 6: afterNth^#(N, XS) -> c_5(snd^#(splitAt(N, XS)))
    , 7: snd^#(pair(X, Y)) -> c_6()
    , 8: and^#(tt(), X) -> c_7()
    , 9: fst^#(pair(X, Y)) -> c_8()
    , 10: head^#(cons(N, XS)) -> c_9()
    , 11: sel^#(N, XS) -> c_11(head^#(afterNth(N, XS)))
    , 12: tail^#(cons(N, XS)) -> c_12()
    , 13: take^#(N, XS) -> c_13(fst^#(splitAt(N, XS))) }

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

Strict DPs: { natsFrom^#(N) -> c_10(natsFrom^#(s(N))) }
Weak DPs:
  { U11^#(tt(), N, X, XS) -> c_1(U12^#(splitAt(N, XS), X))
  , U12^#(pair(YS, ZS), X) -> c_2()
  , splitAt^#(s(N), cons(X, XS)) -> c_3(U11^#(tt(), N, X, XS))
  , splitAt^#(0(), XS) -> c_4()
  , afterNth^#(N, XS) -> c_5(snd^#(splitAt(N, XS)))
  , snd^#(pair(X, Y)) -> c_6()
  , and^#(tt(), X) -> c_7()
  , fst^#(pair(X, Y)) -> c_8()
  , head^#(cons(N, XS)) -> c_9()
  , sel^#(N, XS) -> c_11(head^#(afterNth(N, XS)))
  , tail^#(cons(N, XS)) -> c_12()
  , take^#(N, XS) -> c_13(fst^#(splitAt(N, XS))) }
Weak Trs:
  { U11(tt(), N, X, XS) -> U12(splitAt(N, XS), X)
  , U12(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ U11^#(tt(), N, X, XS) -> c_1(U12^#(splitAt(N, XS), X))
, U12^#(pair(YS, ZS), X) -> c_2()
, splitAt^#(s(N), cons(X, XS)) -> c_3(U11^#(tt(), N, X, XS))
, splitAt^#(0(), XS) -> c_4()
, afterNth^#(N, XS) -> c_5(snd^#(splitAt(N, XS)))
, snd^#(pair(X, Y)) -> c_6()
, and^#(tt(), X) -> c_7()
, fst^#(pair(X, Y)) -> c_8()
, head^#(cons(N, XS)) -> c_9()
, sel^#(N, XS) -> c_11(head^#(afterNth(N, XS)))
, tail^#(cons(N, XS)) -> c_12()
, take^#(N, XS) -> c_13(fst^#(splitAt(N, XS))) }

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

Strict DPs: { natsFrom^#(N) -> c_10(natsFrom^#(s(N))) }
Weak Trs:
  { U11(tt(), N, X, XS) -> U12(splitAt(N, XS), X)
  , U12(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

No rule is usable, rules are removed from the input problem.

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

Strict DPs: { natsFrom^#(N) -> c_10(natsFrom^#(s(N))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..