MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            2nd(mark(X)) -> mark(2nd(X))
            2nd(ok(X)) -> ok(2nd(X))
            active(2nd(X)) -> 2nd(active(X))
            active(2nd(cons(X,cons(Y,Z)))) -> mark(Y)
            active(cons(X1,X2)) -> cons(active(X1),X2)
            active(from(X)) -> from(active(X))
            active(from(X)) -> mark(cons(X,from(s(X))))
            active(s(X)) -> s(active(X))
            cons(mark(X1),X2) -> mark(cons(X1,X2))
            cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
            from(mark(X)) -> mark(from(X))
            from(ok(X)) -> ok(from(X))
            proper(2nd(X)) -> 2nd(proper(X))
            proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
            proper(from(X)) -> from(proper(X))
            proper(s(X)) -> s(proper(X))
            s(mark(X)) -> mark(s(X))
            s(ok(X)) -> ok(s(X))
            top(mark(X)) -> top(proper(X))
            top(ok(X)) -> top(active(X))
        - Signature:
            {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1} / {mark/1,ok/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {2nd,active,cons,from,proper,s,top} and constructors {mark
            ,ok}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          2nd#(mark(X)) -> c_1(2nd#(X))
          2nd#(ok(X)) -> c_2(2nd#(X))
          active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X))
          active#(2nd(cons(X,cons(Y,Z)))) -> c_4()
          active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1))
          active#(from(X)) -> c_6(from#(active(X)),active#(X))
          active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X))
          active#(s(X)) -> c_8(s#(active(X)),active#(X))
          cons#(mark(X1),X2) -> c_9(cons#(X1,X2))
          cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2))
          from#(mark(X)) -> c_11(from#(X))
          from#(ok(X)) -> c_12(from#(X))
          proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X))
          proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
          proper#(from(X)) -> c_15(from#(proper(X)),proper#(X))
          proper#(s(X)) -> c_16(s#(proper(X)),proper#(X))
          s#(mark(X)) -> c_17(s#(X))
          s#(ok(X)) -> c_18(s#(X))
          top#(mark(X)) -> c_19(top#(proper(X)),proper#(X))
          top#(ok(X)) -> c_20(top#(active(X)),active#(X))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            2nd#(mark(X)) -> c_1(2nd#(X))
            2nd#(ok(X)) -> c_2(2nd#(X))
            active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X))
            active#(2nd(cons(X,cons(Y,Z)))) -> c_4()
            active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1))
            active#(from(X)) -> c_6(from#(active(X)),active#(X))
            active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X))
            active#(s(X)) -> c_8(s#(active(X)),active#(X))
            cons#(mark(X1),X2) -> c_9(cons#(X1,X2))
            cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2))
            from#(mark(X)) -> c_11(from#(X))
            from#(ok(X)) -> c_12(from#(X))
            proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X))
            proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
            proper#(from(X)) -> c_15(from#(proper(X)),proper#(X))
            proper#(s(X)) -> c_16(s#(proper(X)),proper#(X))
            s#(mark(X)) -> c_17(s#(X))
            s#(ok(X)) -> c_18(s#(X))
            top#(mark(X)) -> c_19(top#(proper(X)),proper#(X))
            top#(ok(X)) -> c_20(top#(active(X)),active#(X))
        - Weak TRS:
            2nd(mark(X)) -> mark(2nd(X))
            2nd(ok(X)) -> ok(2nd(X))
            active(2nd(X)) -> 2nd(active(X))
            active(2nd(cons(X,cons(Y,Z)))) -> mark(Y)
            active(cons(X1,X2)) -> cons(active(X1),X2)
            active(from(X)) -> from(active(X))
            active(from(X)) -> mark(cons(X,from(s(X))))
            active(s(X)) -> s(active(X))
            cons(mark(X1),X2) -> mark(cons(X1,X2))
            cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
            from(mark(X)) -> mark(from(X))
            from(ok(X)) -> ok(from(X))
            proper(2nd(X)) -> 2nd(proper(X))
            proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
            proper(from(X)) -> from(proper(X))
            proper(s(X)) -> s(proper(X))
            s(mark(X)) -> mark(s(X))
            s(ok(X)) -> ok(s(X))
            top(mark(X)) -> top(proper(X))
            top(ok(X)) -> top(active(X))
        - Signature:
            {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1
            ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2
            ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s#
            ,top#} and constructors {mark,ok}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          2nd(mark(X)) -> mark(2nd(X))
          2nd(ok(X)) -> ok(2nd(X))
          active(2nd(X)) -> 2nd(active(X))
          active(2nd(cons(X,cons(Y,Z)))) -> mark(Y)
          active(cons(X1,X2)) -> cons(active(X1),X2)
          active(from(X)) -> from(active(X))
          active(from(X)) -> mark(cons(X,from(s(X))))
          active(s(X)) -> s(active(X))
          cons(mark(X1),X2) -> mark(cons(X1,X2))
          cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
          from(mark(X)) -> mark(from(X))
          from(ok(X)) -> ok(from(X))
          proper(2nd(X)) -> 2nd(proper(X))
          proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
          proper(from(X)) -> from(proper(X))
          proper(s(X)) -> s(proper(X))
          s(mark(X)) -> mark(s(X))
          s(ok(X)) -> ok(s(X))
          2nd#(mark(X)) -> c_1(2nd#(X))
          2nd#(ok(X)) -> c_2(2nd#(X))
          active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X))
          active#(2nd(cons(X,cons(Y,Z)))) -> c_4()
          active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1))
          active#(from(X)) -> c_6(from#(active(X)),active#(X))
          active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X))
          active#(s(X)) -> c_8(s#(active(X)),active#(X))
          cons#(mark(X1),X2) -> c_9(cons#(X1,X2))
          cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2))
          from#(mark(X)) -> c_11(from#(X))
          from#(ok(X)) -> c_12(from#(X))
          proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X))
          proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
          proper#(from(X)) -> c_15(from#(proper(X)),proper#(X))
          proper#(s(X)) -> c_16(s#(proper(X)),proper#(X))
          s#(mark(X)) -> c_17(s#(X))
          s#(ok(X)) -> c_18(s#(X))
          top#(mark(X)) -> c_19(top#(proper(X)),proper#(X))
          top#(ok(X)) -> c_20(top#(active(X)),active#(X))
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            2nd#(mark(X)) -> c_1(2nd#(X))
            2nd#(ok(X)) -> c_2(2nd#(X))
            active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X))
            active#(2nd(cons(X,cons(Y,Z)))) -> c_4()
            active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1))
            active#(from(X)) -> c_6(from#(active(X)),active#(X))
            active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X))
            active#(s(X)) -> c_8(s#(active(X)),active#(X))
            cons#(mark(X1),X2) -> c_9(cons#(X1,X2))
            cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2))
            from#(mark(X)) -> c_11(from#(X))
            from#(ok(X)) -> c_12(from#(X))
            proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X))
            proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
            proper#(from(X)) -> c_15(from#(proper(X)),proper#(X))
            proper#(s(X)) -> c_16(s#(proper(X)),proper#(X))
            s#(mark(X)) -> c_17(s#(X))
            s#(ok(X)) -> c_18(s#(X))
            top#(mark(X)) -> c_19(top#(proper(X)),proper#(X))
            top#(ok(X)) -> c_20(top#(active(X)),active#(X))
        - Weak TRS:
            2nd(mark(X)) -> mark(2nd(X))
            2nd(ok(X)) -> ok(2nd(X))
            active(2nd(X)) -> 2nd(active(X))
            active(2nd(cons(X,cons(Y,Z)))) -> mark(Y)
            active(cons(X1,X2)) -> cons(active(X1),X2)
            active(from(X)) -> from(active(X))
            active(from(X)) -> mark(cons(X,from(s(X))))
            active(s(X)) -> s(active(X))
            cons(mark(X1),X2) -> mark(cons(X1,X2))
            cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
            from(mark(X)) -> mark(from(X))
            from(ok(X)) -> ok(from(X))
            proper(2nd(X)) -> 2nd(proper(X))
            proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
            proper(from(X)) -> from(proper(X))
            proper(s(X)) -> s(proper(X))
            s(mark(X)) -> mark(s(X))
            s(ok(X)) -> ok(s(X))
        - Signature:
            {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1
            ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2
            ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s#
            ,top#} and constructors {mark,ok}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {4}
        by application of
          Pre({4}) = {3,5,6,8,20}.
        Here rules are labelled as follows:
          1: 2nd#(mark(X)) -> c_1(2nd#(X))
          2: 2nd#(ok(X)) -> c_2(2nd#(X))
          3: active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X))
          4: active#(2nd(cons(X,cons(Y,Z)))) -> c_4()
          5: active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1))
          6: active#(from(X)) -> c_6(from#(active(X)),active#(X))
          7: active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X))
          8: active#(s(X)) -> c_8(s#(active(X)),active#(X))
          9: cons#(mark(X1),X2) -> c_9(cons#(X1,X2))
          10: cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2))
          11: from#(mark(X)) -> c_11(from#(X))
          12: from#(ok(X)) -> c_12(from#(X))
          13: proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X))
          14: proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
          15: proper#(from(X)) -> c_15(from#(proper(X)),proper#(X))
          16: proper#(s(X)) -> c_16(s#(proper(X)),proper#(X))
          17: s#(mark(X)) -> c_17(s#(X))
          18: s#(ok(X)) -> c_18(s#(X))
          19: top#(mark(X)) -> c_19(top#(proper(X)),proper#(X))
          20: top#(ok(X)) -> c_20(top#(active(X)),active#(X))
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            2nd#(mark(X)) -> c_1(2nd#(X))
            2nd#(ok(X)) -> c_2(2nd#(X))
            active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X))
            active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1))
            active#(from(X)) -> c_6(from#(active(X)),active#(X))
            active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X))
            active#(s(X)) -> c_8(s#(active(X)),active#(X))
            cons#(mark(X1),X2) -> c_9(cons#(X1,X2))
            cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2))
            from#(mark(X)) -> c_11(from#(X))
            from#(ok(X)) -> c_12(from#(X))
            proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X))
            proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
            proper#(from(X)) -> c_15(from#(proper(X)),proper#(X))
            proper#(s(X)) -> c_16(s#(proper(X)),proper#(X))
            s#(mark(X)) -> c_17(s#(X))
            s#(ok(X)) -> c_18(s#(X))
            top#(mark(X)) -> c_19(top#(proper(X)),proper#(X))
            top#(ok(X)) -> c_20(top#(active(X)),active#(X))
        - Weak DPs:
            active#(2nd(cons(X,cons(Y,Z)))) -> c_4()
        - Weak TRS:
            2nd(mark(X)) -> mark(2nd(X))
            2nd(ok(X)) -> ok(2nd(X))
            active(2nd(X)) -> 2nd(active(X))
            active(2nd(cons(X,cons(Y,Z)))) -> mark(Y)
            active(cons(X1,X2)) -> cons(active(X1),X2)
            active(from(X)) -> from(active(X))
            active(from(X)) -> mark(cons(X,from(s(X))))
            active(s(X)) -> s(active(X))
            cons(mark(X1),X2) -> mark(cons(X1,X2))
            cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
            from(mark(X)) -> mark(from(X))
            from(ok(X)) -> ok(from(X))
            proper(2nd(X)) -> 2nd(proper(X))
            proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
            proper(from(X)) -> from(proper(X))
            proper(s(X)) -> s(proper(X))
            s(mark(X)) -> mark(s(X))
            s(ok(X)) -> ok(s(X))
        - Signature:
            {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1
            ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2
            ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s#
            ,top#} and constructors {mark,ok}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:2nd#(mark(X)) -> c_1(2nd#(X))
             -->_1 2nd#(ok(X)) -> c_2(2nd#(X)):2
             -->_1 2nd#(mark(X)) -> c_1(2nd#(X)):1
          
          2:S:2nd#(ok(X)) -> c_2(2nd#(X))
             -->_1 2nd#(ok(X)) -> c_2(2nd#(X)):2
             -->_1 2nd#(mark(X)) -> c_1(2nd#(X)):1
          
          3:S:active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X))
             -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):7
             -->_2 active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)):6
             -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):5
             -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):4
             -->_2 active#(2nd(cons(X,cons(Y,Z)))) -> c_4():20
             -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3
             -->_1 2nd#(ok(X)) -> c_2(2nd#(X)):2
             -->_1 2nd#(mark(X)) -> c_1(2nd#(X)):1
          
          4:S:active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1))
             -->_1 cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)):9
             -->_1 cons#(mark(X1),X2) -> c_9(cons#(X1,X2)):8
             -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):7
             -->_2 active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)):6
             -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):5
             -->_2 active#(2nd(cons(X,cons(Y,Z)))) -> c_4():20
             -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):4
             -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3
          
          5:S:active#(from(X)) -> c_6(from#(active(X)),active#(X))
             -->_1 from#(ok(X)) -> c_12(from#(X)):11
             -->_1 from#(mark(X)) -> c_11(from#(X)):10
             -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):7
             -->_2 active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)):6
             -->_2 active#(2nd(cons(X,cons(Y,Z)))) -> c_4():20
             -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):5
             -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):4
             -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3
          
          6:S:active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X))
             -->_3 s#(ok(X)) -> c_18(s#(X)):17
             -->_3 s#(mark(X)) -> c_17(s#(X)):16
             -->_2 from#(ok(X)) -> c_12(from#(X)):11
             -->_2 from#(mark(X)) -> c_11(from#(X)):10
             -->_1 cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)):9
             -->_1 cons#(mark(X1),X2) -> c_9(cons#(X1,X2)):8
          
          7:S:active#(s(X)) -> c_8(s#(active(X)),active#(X))
             -->_1 s#(ok(X)) -> c_18(s#(X)):17
             -->_1 s#(mark(X)) -> c_17(s#(X)):16
             -->_2 active#(2nd(cons(X,cons(Y,Z)))) -> c_4():20
             -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):7
             -->_2 active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)):6
             -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):5
             -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):4
             -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3
          
          8:S:cons#(mark(X1),X2) -> c_9(cons#(X1,X2))
             -->_1 cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)):9
             -->_1 cons#(mark(X1),X2) -> c_9(cons#(X1,X2)):8
          
          9:S:cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2))
             -->_1 cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)):9
             -->_1 cons#(mark(X1),X2) -> c_9(cons#(X1,X2)):8
          
          10:S:from#(mark(X)) -> c_11(from#(X))
             -->_1 from#(ok(X)) -> c_12(from#(X)):11
             -->_1 from#(mark(X)) -> c_11(from#(X)):10
          
          11:S:from#(ok(X)) -> c_12(from#(X))
             -->_1 from#(ok(X)) -> c_12(from#(X)):11
             -->_1 from#(mark(X)) -> c_11(from#(X)):10
          
          12:S:proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X))
             -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):15
             -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):14
             -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):13
             -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):12
             -->_1 2nd#(ok(X)) -> c_2(2nd#(X)):2
             -->_1 2nd#(mark(X)) -> c_1(2nd#(X)):1
          
          13:S:proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
             -->_3 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):15
             -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):15
             -->_3 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):14
             -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):14
             -->_3 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):13
             -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):13
             -->_3 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):12
             -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):12
             -->_1 cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)):9
             -->_1 cons#(mark(X1),X2) -> c_9(cons#(X1,X2)):8
          
          14:S:proper#(from(X)) -> c_15(from#(proper(X)),proper#(X))
             -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):15
             -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):14
             -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):13
             -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):12
             -->_1 from#(ok(X)) -> c_12(from#(X)):11
             -->_1 from#(mark(X)) -> c_11(from#(X)):10
          
          15:S:proper#(s(X)) -> c_16(s#(proper(X)),proper#(X))
             -->_1 s#(ok(X)) -> c_18(s#(X)):17
             -->_1 s#(mark(X)) -> c_17(s#(X)):16
             -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):15
             -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):14
             -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):13
             -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):12
          
          16:S:s#(mark(X)) -> c_17(s#(X))
             -->_1 s#(ok(X)) -> c_18(s#(X)):17
             -->_1 s#(mark(X)) -> c_17(s#(X)):16
          
          17:S:s#(ok(X)) -> c_18(s#(X))
             -->_1 s#(ok(X)) -> c_18(s#(X)):17
             -->_1 s#(mark(X)) -> c_17(s#(X)):16
          
          18:S:top#(mark(X)) -> c_19(top#(proper(X)),proper#(X))
             -->_1 top#(ok(X)) -> c_20(top#(active(X)),active#(X)):19
             -->_1 top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)):18
             -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):15
             -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):14
             -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):13
             -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):12
          
          19:S:top#(ok(X)) -> c_20(top#(active(X)),active#(X))
             -->_2 active#(2nd(cons(X,cons(Y,Z)))) -> c_4():20
             -->_1 top#(ok(X)) -> c_20(top#(active(X)),active#(X)):19
             -->_1 top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)):18
             -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):7
             -->_2 active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)):6
             -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):5
             -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):4
             -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3
          
          20:W:active#(2nd(cons(X,cons(Y,Z)))) -> c_4()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          20: active#(2nd(cons(X,cons(Y,Z)))) -> c_4()
* Step 5: NaturalMI MAYBE
    + Considered Problem:
        - Strict DPs:
            2nd#(mark(X)) -> c_1(2nd#(X))
            2nd#(ok(X)) -> c_2(2nd#(X))
            active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X))
            active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1))
            active#(from(X)) -> c_6(from#(active(X)),active#(X))
            active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X))
            active#(s(X)) -> c_8(s#(active(X)),active#(X))
            cons#(mark(X1),X2) -> c_9(cons#(X1,X2))
            cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2))
            from#(mark(X)) -> c_11(from#(X))
            from#(ok(X)) -> c_12(from#(X))
            proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X))
            proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
            proper#(from(X)) -> c_15(from#(proper(X)),proper#(X))
            proper#(s(X)) -> c_16(s#(proper(X)),proper#(X))
            s#(mark(X)) -> c_17(s#(X))
            s#(ok(X)) -> c_18(s#(X))
            top#(mark(X)) -> c_19(top#(proper(X)),proper#(X))
            top#(ok(X)) -> c_20(top#(active(X)),active#(X))
        - Weak TRS:
            2nd(mark(X)) -> mark(2nd(X))
            2nd(ok(X)) -> ok(2nd(X))
            active(2nd(X)) -> 2nd(active(X))
            active(2nd(cons(X,cons(Y,Z)))) -> mark(Y)
            active(cons(X1,X2)) -> cons(active(X1),X2)
            active(from(X)) -> from(active(X))
            active(from(X)) -> mark(cons(X,from(s(X))))
            active(s(X)) -> s(active(X))
            cons(mark(X1),X2) -> mark(cons(X1,X2))
            cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
            from(mark(X)) -> mark(from(X))
            from(ok(X)) -> ok(from(X))
            proper(2nd(X)) -> 2nd(proper(X))
            proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
            proper(from(X)) -> from(proper(X))
            proper(s(X)) -> s(proper(X))
            s(mark(X)) -> mark(s(X))
            s(ok(X)) -> ok(s(X))
        - Signature:
            {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1
            ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2
            ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s#
            ,top#} and constructors {mark,ok}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_2) = {1},
          uargs(c_3) = {1,2},
          uargs(c_5) = {1,2},
          uargs(c_6) = {1,2},
          uargs(c_7) = {1,2,3},
          uargs(c_8) = {1,2},
          uargs(c_9) = {1},
          uargs(c_10) = {1},
          uargs(c_11) = {1},
          uargs(c_12) = {1},
          uargs(c_13) = {1,2},
          uargs(c_14) = {1,2,3},
          uargs(c_15) = {1,2},
          uargs(c_16) = {1,2},
          uargs(c_17) = {1},
          uargs(c_18) = {1},
          uargs(c_19) = {1,2},
          uargs(c_20) = {1,2}
        
        Following symbols are considered usable:
          {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#}
        TcT has computed the following interpretation:
              p(2nd) = [2] x1 + [0]                  
           p(active) = [0]                           
             p(cons) = [2] x1 + [0]                  
             p(from) = [4] x1 + [0]                  
             p(mark) = [0]                           
               p(ok) = [3]                           
           p(proper) = [0]                           
                p(s) = [1] x1 + [0]                  
              p(top) = [1] x1 + [1]                  
             p(2nd#) = [0]                           
          p(active#) = [2]                           
            p(cons#) = [0]                           
            p(from#) = [0]                           
          p(proper#) = [0]                           
               p(s#) = [0]                           
             p(top#) = [5] x1 + [0]                  
              p(c_1) = [4] x1 + [0]                  
              p(c_2) = [2] x1 + [0]                  
              p(c_3) = [1] x1 + [1] x2 + [0]         
              p(c_4) = [2]                           
              p(c_5) = [2] x1 + [1] x2 + [0]         
              p(c_6) = [1] x1 + [1] x2 + [0]         
              p(c_7) = [4] x1 + [4] x2 + [1] x3 + [0]
              p(c_8) = [4] x1 + [1] x2 + [0]         
              p(c_9) = [2] x1 + [0]                  
             p(c_10) = [4] x1 + [0]                  
             p(c_11) = [4] x1 + [0]                  
             p(c_12) = [4] x1 + [0]                  
             p(c_13) = [4] x1 + [4] x2 + [0]         
             p(c_14) = [2] x1 + [4] x2 + [1] x3 + [0]
             p(c_15) = [1] x1 + [2] x2 + [0]         
             p(c_16) = [4] x1 + [2] x2 + [0]         
             p(c_17) = [2] x1 + [0]                  
             p(c_18) = [2] x1 + [0]                  
             p(c_19) = [1] x1 + [2] x2 + [0]         
             p(c_20) = [4] x1 + [4] x2 + [5]         
        
        Following rules are strictly oriented:
        active#(from(X)) = [2]                                       
                         > [0]                                       
                         = c_7(cons#(X,from(s(X))),from#(s(X)),s#(X))
        
             top#(ok(X)) = [15]                                      
                         > [13]                                      
                         = c_20(top#(active(X)),active#(X))          
        
        
        Following rules are (at-least) weakly oriented:
                         2nd#(mark(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_1(2nd#(X))                                              
        
                           2nd#(ok(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_2(2nd#(X))                                              
        
                       active#(2nd(X)) =  [2]                                                       
                                       >= [2]                                                       
                                       =  c_3(2nd#(active(X)),active#(X))                           
        
                  active#(cons(X1,X2)) =  [2]                                                       
                                       >= [2]                                                       
                                       =  c_5(cons#(active(X1),X2),active#(X1))                     
        
                      active#(from(X)) =  [2]                                                       
                                       >= [2]                                                       
                                       =  c_6(from#(active(X)),active#(X))                          
        
                         active#(s(X)) =  [2]                                                       
                                       >= [2]                                                       
                                       =  c_8(s#(active(X)),active#(X))                             
        
                    cons#(mark(X1),X2) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_9(cons#(X1,X2))                                         
        
                  cons#(ok(X1),ok(X2)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_10(cons#(X1,X2))                                        
        
                        from#(mark(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_11(from#(X))                                            
        
                          from#(ok(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_12(from#(X))                                            
        
                       proper#(2nd(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_13(2nd#(proper(X)),proper#(X))                          
        
                  proper#(cons(X1,X2)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
        
                      proper#(from(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_15(from#(proper(X)),proper#(X))                         
        
                         proper#(s(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_16(s#(proper(X)),proper#(X))                            
        
                           s#(mark(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_17(s#(X))                                               
        
                             s#(ok(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_18(s#(X))                                               
        
                         top#(mark(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_19(top#(proper(X)),proper#(X))                          
        
                          2nd(mark(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  mark(2nd(X))                                              
        
                            2nd(ok(X)) =  [6]                                                       
                                       >= [3]                                                       
                                       =  ok(2nd(X))                                                
        
                        active(2nd(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  2nd(active(X))                                            
        
        active(2nd(cons(X,cons(Y,Z)))) =  [0]                                                       
                                       >= [0]                                                       
                                       =  mark(Y)                                                   
        
                   active(cons(X1,X2)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  cons(active(X1),X2)                                       
        
                       active(from(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  from(active(X))                                           
        
                       active(from(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  mark(cons(X,from(s(X))))                                  
        
                          active(s(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  s(active(X))                                              
        
                     cons(mark(X1),X2) =  [0]                                                       
                                       >= [0]                                                       
                                       =  mark(cons(X1,X2))                                         
        
                   cons(ok(X1),ok(X2)) =  [6]                                                       
                                       >= [3]                                                       
                                       =  ok(cons(X1,X2))                                           
        
                         from(mark(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  mark(from(X))                                             
        
                           from(ok(X)) =  [12]                                                      
                                       >= [3]                                                       
                                       =  ok(from(X))                                               
        
                        proper(2nd(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  2nd(proper(X))                                            
        
                   proper(cons(X1,X2)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  cons(proper(X1),proper(X2))                               
        
                       proper(from(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  from(proper(X))                                           
        
                          proper(s(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  s(proper(X))                                              
        
                            s(mark(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  mark(s(X))                                                
        
                              s(ok(X)) =  [3]                                                       
                                       >= [3]                                                       
                                       =  ok(s(X))                                                  
        
* Step 6: NaturalMI MAYBE
    + Considered Problem:
        - Strict DPs:
            2nd#(mark(X)) -> c_1(2nd#(X))
            2nd#(ok(X)) -> c_2(2nd#(X))
            active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X))
            active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1))
            active#(from(X)) -> c_6(from#(active(X)),active#(X))
            active#(s(X)) -> c_8(s#(active(X)),active#(X))
            cons#(mark(X1),X2) -> c_9(cons#(X1,X2))
            cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2))
            from#(mark(X)) -> c_11(from#(X))
            from#(ok(X)) -> c_12(from#(X))
            proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X))
            proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
            proper#(from(X)) -> c_15(from#(proper(X)),proper#(X))
            proper#(s(X)) -> c_16(s#(proper(X)),proper#(X))
            s#(mark(X)) -> c_17(s#(X))
            s#(ok(X)) -> c_18(s#(X))
            top#(mark(X)) -> c_19(top#(proper(X)),proper#(X))
        - Weak DPs:
            active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X))
            top#(ok(X)) -> c_20(top#(active(X)),active#(X))
        - Weak TRS:
            2nd(mark(X)) -> mark(2nd(X))
            2nd(ok(X)) -> ok(2nd(X))
            active(2nd(X)) -> 2nd(active(X))
            active(2nd(cons(X,cons(Y,Z)))) -> mark(Y)
            active(cons(X1,X2)) -> cons(active(X1),X2)
            active(from(X)) -> from(active(X))
            active(from(X)) -> mark(cons(X,from(s(X))))
            active(s(X)) -> s(active(X))
            cons(mark(X1),X2) -> mark(cons(X1,X2))
            cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
            from(mark(X)) -> mark(from(X))
            from(ok(X)) -> ok(from(X))
            proper(2nd(X)) -> 2nd(proper(X))
            proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
            proper(from(X)) -> from(proper(X))
            proper(s(X)) -> s(proper(X))
            s(mark(X)) -> mark(s(X))
            s(ok(X)) -> ok(s(X))
        - Signature:
            {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1
            ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2
            ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s#
            ,top#} and constructors {mark,ok}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_2) = {1},
          uargs(c_3) = {1,2},
          uargs(c_5) = {1,2},
          uargs(c_6) = {1,2},
          uargs(c_7) = {1,2,3},
          uargs(c_8) = {1,2},
          uargs(c_9) = {1},
          uargs(c_10) = {1},
          uargs(c_11) = {1},
          uargs(c_12) = {1},
          uargs(c_13) = {1,2},
          uargs(c_14) = {1,2,3},
          uargs(c_15) = {1,2},
          uargs(c_16) = {1,2},
          uargs(c_17) = {1},
          uargs(c_18) = {1},
          uargs(c_19) = {1,2},
          uargs(c_20) = {1,2}
        
        Following symbols are considered usable:
          {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#}
        TcT has computed the following interpretation:
              p(2nd) = [1] x1 + [0]                  
           p(active) = [1]                           
             p(cons) = [1] x1 + [0]                  
             p(from) = [1] x1 + [0]                  
             p(mark) = [1]                           
               p(ok) = [4]                           
           p(proper) = [0]                           
                p(s) = [1] x1 + [0]                  
              p(top) = [2] x1 + [2]                  
             p(2nd#) = [0]                           
          p(active#) = [0]                           
            p(cons#) = [0]                           
            p(from#) = [0]                           
          p(proper#) = [0]                           
               p(s#) = [0]                           
             p(top#) = [2] x1 + [4]                  
              p(c_1) = [4] x1 + [0]                  
              p(c_2) = [4] x1 + [0]                  
              p(c_3) = [2] x1 + [2] x2 + [0]         
              p(c_4) = [0]                           
              p(c_5) = [4] x1 + [4] x2 + [0]         
              p(c_6) = [4] x1 + [1] x2 + [0]         
              p(c_7) = [1] x1 + [2] x2 + [1] x3 + [0]
              p(c_8) = [1] x1 + [1] x2 + [0]         
              p(c_9) = [2] x1 + [0]                  
             p(c_10) = [4] x1 + [0]                  
             p(c_11) = [4] x1 + [0]                  
             p(c_12) = [4] x1 + [0]                  
             p(c_13) = [1] x1 + [4] x2 + [0]         
             p(c_14) = [2] x1 + [4] x2 + [2] x3 + [0]
             p(c_15) = [2] x1 + [1] x2 + [0]         
             p(c_16) = [4] x1 + [1] x2 + [0]         
             p(c_17) = [1] x1 + [0]                  
             p(c_18) = [4] x1 + [0]                  
             p(c_19) = [1] x1 + [2] x2 + [0]         
             p(c_20) = [2] x1 + [4] x2 + [0]         
        
        Following rules are strictly oriented:
        top#(mark(X)) = [6]                             
                      > [4]                             
                      = c_19(top#(proper(X)),proper#(X))
        
        
        Following rules are (at-least) weakly oriented:
                         2nd#(mark(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_1(2nd#(X))                                              
        
                           2nd#(ok(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_2(2nd#(X))                                              
        
                       active#(2nd(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_3(2nd#(active(X)),active#(X))                           
        
                  active#(cons(X1,X2)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_5(cons#(active(X1),X2),active#(X1))                     
        
                      active#(from(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_6(from#(active(X)),active#(X))                          
        
                      active#(from(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_7(cons#(X,from(s(X))),from#(s(X)),s#(X))                
        
                         active#(s(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_8(s#(active(X)),active#(X))                             
        
                    cons#(mark(X1),X2) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_9(cons#(X1,X2))                                         
        
                  cons#(ok(X1),ok(X2)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_10(cons#(X1,X2))                                        
        
                        from#(mark(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_11(from#(X))                                            
        
                          from#(ok(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_12(from#(X))                                            
        
                       proper#(2nd(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_13(2nd#(proper(X)),proper#(X))                          
        
                  proper#(cons(X1,X2)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
        
                      proper#(from(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_15(from#(proper(X)),proper#(X))                         
        
                         proper#(s(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_16(s#(proper(X)),proper#(X))                            
        
                           s#(mark(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_17(s#(X))                                               
        
                             s#(ok(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  c_18(s#(X))                                               
        
                           top#(ok(X)) =  [12]                                                      
                                       >= [12]                                                      
                                       =  c_20(top#(active(X)),active#(X))                          
        
                          2nd(mark(X)) =  [1]                                                       
                                       >= [1]                                                       
                                       =  mark(2nd(X))                                              
        
                            2nd(ok(X)) =  [4]                                                       
                                       >= [4]                                                       
                                       =  ok(2nd(X))                                                
        
                        active(2nd(X)) =  [1]                                                       
                                       >= [1]                                                       
                                       =  2nd(active(X))                                            
        
        active(2nd(cons(X,cons(Y,Z)))) =  [1]                                                       
                                       >= [1]                                                       
                                       =  mark(Y)                                                   
        
                   active(cons(X1,X2)) =  [1]                                                       
                                       >= [1]                                                       
                                       =  cons(active(X1),X2)                                       
        
                       active(from(X)) =  [1]                                                       
                                       >= [1]                                                       
                                       =  from(active(X))                                           
        
                       active(from(X)) =  [1]                                                       
                                       >= [1]                                                       
                                       =  mark(cons(X,from(s(X))))                                  
        
                          active(s(X)) =  [1]                                                       
                                       >= [1]                                                       
                                       =  s(active(X))                                              
        
                     cons(mark(X1),X2) =  [1]                                                       
                                       >= [1]                                                       
                                       =  mark(cons(X1,X2))                                         
        
                   cons(ok(X1),ok(X2)) =  [4]                                                       
                                       >= [4]                                                       
                                       =  ok(cons(X1,X2))                                           
        
                         from(mark(X)) =  [1]                                                       
                                       >= [1]                                                       
                                       =  mark(from(X))                                             
        
                           from(ok(X)) =  [4]                                                       
                                       >= [4]                                                       
                                       =  ok(from(X))                                               
        
                        proper(2nd(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  2nd(proper(X))                                            
        
                   proper(cons(X1,X2)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  cons(proper(X1),proper(X2))                               
        
                       proper(from(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  from(proper(X))                                           
        
                          proper(s(X)) =  [0]                                                       
                                       >= [0]                                                       
                                       =  s(proper(X))                                              
        
                            s(mark(X)) =  [1]                                                       
                                       >= [1]                                                       
                                       =  mark(s(X))                                                
        
                              s(ok(X)) =  [4]                                                       
                                       >= [4]                                                       
                                       =  ok(s(X))                                                  
        
* Step 7: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          2nd#(mark(X)) -> c_1(2nd#(X))
          2nd#(ok(X)) -> c_2(2nd#(X))
          active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X))
          active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1))
          active#(from(X)) -> c_6(from#(active(X)),active#(X))
          active#(s(X)) -> c_8(s#(active(X)),active#(X))
          cons#(mark(X1),X2) -> c_9(cons#(X1,X2))
          cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2))
          from#(mark(X)) -> c_11(from#(X))
          from#(ok(X)) -> c_12(from#(X))
          proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X))
          proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2))
          proper#(from(X)) -> c_15(from#(proper(X)),proper#(X))
          proper#(s(X)) -> c_16(s#(proper(X)),proper#(X))
          s#(mark(X)) -> c_17(s#(X))
          s#(ok(X)) -> c_18(s#(X))
      - Weak DPs:
          active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X))
          top#(mark(X)) -> c_19(top#(proper(X)),proper#(X))
          top#(ok(X)) -> c_20(top#(active(X)),active#(X))
      - Weak TRS:
          2nd(mark(X)) -> mark(2nd(X))
          2nd(ok(X)) -> ok(2nd(X))
          active(2nd(X)) -> 2nd(active(X))
          active(2nd(cons(X,cons(Y,Z)))) -> mark(Y)
          active(cons(X1,X2)) -> cons(active(X1),X2)
          active(from(X)) -> from(active(X))
          active(from(X)) -> mark(cons(X,from(s(X))))
          active(s(X)) -> s(active(X))
          cons(mark(X1),X2) -> mark(cons(X1,X2))
          cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
          from(mark(X)) -> mark(from(X))
          from(ok(X)) -> ok(from(X))
          proper(2nd(X)) -> 2nd(proper(X))
          proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
          proper(from(X)) -> from(proper(X))
          proper(s(X)) -> s(proper(X))
          s(mark(X)) -> mark(s(X))
          s(ok(X)) -> ok(s(X))
      - Signature:
          {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1
          ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2
          ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s#
          ,top#} and constructors {mark,ok}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE