MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            a__U11(X1,X2) -> U11(X1,X2)
            a__U11(tt(),V2) -> a__U12(a__isNat(V2))
            a__U12(X) -> U12(X)
            a__U12(tt()) -> tt()
            a__U21(X) -> U21(X)
            a__U21(tt()) -> tt()
            a__U31(X1,X2) -> U31(X1,X2)
            a__U31(tt(),V2) -> a__U32(a__isNat(V2))
            a__U32(X) -> U32(X)
            a__U32(tt()) -> tt()
            a__U41(X1,X2) -> U41(X1,X2)
            a__U41(tt(),N) -> mark(N)
            a__U51(X1,X2,X3) -> U51(X1,X2,X3)
            a__U51(tt(),M,N) -> a__U52(a__isNat(N),M,N)
            a__U52(X1,X2,X3) -> U52(X1,X2,X3)
            a__U52(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
            a__U61(X) -> U61(X)
            a__U61(tt()) -> 0()
            a__U71(X1,X2,X3) -> U71(X1,X2,X3)
            a__U71(tt(),M,N) -> a__U72(a__isNat(N),M,N)
            a__U72(X1,X2,X3) -> U72(X1,X2,X3)
            a__U72(tt(),M,N) -> a__plus(a__x(mark(N),mark(M)),mark(N))
            a__isNat(X) -> isNat(X)
            a__isNat(0()) -> tt()
            a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
            a__isNat(s(V1)) -> a__U21(a__isNat(V1))
            a__isNat(x(V1,V2)) -> a__U31(a__isNat(V1),V2)
            a__plus(N,0()) -> a__U41(a__isNat(N),N)
            a__plus(N,s(M)) -> a__U51(a__isNat(M),M,N)
            a__plus(X1,X2) -> plus(X1,X2)
            a__x(N,0()) -> a__U61(a__isNat(N))
            a__x(N,s(M)) -> a__U71(a__isNat(M),M,N)
            a__x(X1,X2) -> x(X1,X2)
            mark(0()) -> 0()
            mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
            mark(U12(X)) -> a__U12(mark(X))
            mark(U21(X)) -> a__U21(mark(X))
            mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
            mark(U32(X)) -> a__U32(mark(X))
            mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
            mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
            mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
            mark(U61(X)) -> a__U61(mark(X))
            mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
            mark(U72(X1,X2,X3)) -> a__U72(mark(X1),X2,X3)
            mark(isNat(X)) -> a__isNat(X)
            mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
            mark(s(X)) -> s(mark(X))
            mark(tt()) -> tt()
            mark(x(X1,X2)) -> a__x(mark(X1),mark(X2))
        - Signature:
            {a__U11/2,a__U12/1,a__U21/1,a__U31/2,a__U32/1,a__U41/2,a__U51/3,a__U52/3,a__U61/1,a__U71/3,a__U72/3
            ,a__isNat/1,a__plus/2,a__x/2,mark/1} / {0/0,U11/2,U12/1,U21/1,U31/2,U32/1,U41/2,U51/3,U52/3,U61/1,U71/3
            ,U72/3,isNat/1,plus/2,s/1,tt/0,x/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__U11,a__U12,a__U21,a__U31,a__U32,a__U41,a__U51,a__U52
            ,a__U61,a__U71,a__U72,a__isNat,a__plus,a__x,mark} and constructors {0,U11,U12,U21,U31,U32,U41,U51,U52,U61
            ,U71,U72,isNat,plus,s,tt,x}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          a__U11#(X1,X2) -> c_1()
          a__U11#(tt(),V2) -> c_2(a__U12#(a__isNat(V2)),a__isNat#(V2))
          a__U12#(X) -> c_3()
          a__U12#(tt()) -> c_4()
          a__U21#(X) -> c_5()
          a__U21#(tt()) -> c_6()
          a__U31#(X1,X2) -> c_7()
          a__U31#(tt(),V2) -> c_8(a__U32#(a__isNat(V2)),a__isNat#(V2))
          a__U32#(X) -> c_9()
          a__U32#(tt()) -> c_10()
          a__U41#(X1,X2) -> c_11()
          a__U41#(tt(),N) -> c_12(mark#(N))
          a__U51#(X1,X2,X3) -> c_13()
          a__U51#(tt(),M,N) -> c_14(a__U52#(a__isNat(N),M,N),a__isNat#(N))
          a__U52#(X1,X2,X3) -> c_15()
          a__U52#(tt(),M,N) -> c_16(a__plus#(mark(N),mark(M)),mark#(N),mark#(M))
          a__U61#(X) -> c_17()
          a__U61#(tt()) -> c_18()
          a__U71#(X1,X2,X3) -> c_19()
          a__U71#(tt(),M,N) -> c_20(a__U72#(a__isNat(N),M,N),a__isNat#(N))
          a__U72#(X1,X2,X3) -> c_21()
          a__U72#(tt(),M,N) -> c_22(a__plus#(a__x(mark(N),mark(M)),mark(N))
                                   ,a__x#(mark(N),mark(M))
                                   ,mark#(N)
                                   ,mark#(M)
                                   ,mark#(N))
          a__isNat#(X) -> c_23()
          a__isNat#(0()) -> c_24()
          a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1))
          a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1))
          a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1))
          a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N))
          a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M))
          a__plus#(X1,X2) -> c_30()
          a__x#(N,0()) -> c_31(a__U61#(a__isNat(N)),a__isNat#(N))
          a__x#(N,s(M)) -> c_32(a__U71#(a__isNat(M),M,N),a__isNat#(M))
          a__x#(X1,X2) -> c_33()
          mark#(0()) -> c_34()
          mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1))
          mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X))
          mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X))
          mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1))
          mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X))
          mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1))
          mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1))
          mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1))
          mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X))
          mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1))
          mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1))
          mark#(isNat(X)) -> c_46(a__isNat#(X))
          mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
          mark#(s(X)) -> c_48(mark#(X))
          mark#(tt()) -> c_49()
          mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            a__U11#(X1,X2) -> c_1()
            a__U11#(tt(),V2) -> c_2(a__U12#(a__isNat(V2)),a__isNat#(V2))
            a__U12#(X) -> c_3()
            a__U12#(tt()) -> c_4()
            a__U21#(X) -> c_5()
            a__U21#(tt()) -> c_6()
            a__U31#(X1,X2) -> c_7()
            a__U31#(tt(),V2) -> c_8(a__U32#(a__isNat(V2)),a__isNat#(V2))
            a__U32#(X) -> c_9()
            a__U32#(tt()) -> c_10()
            a__U41#(X1,X2) -> c_11()
            a__U41#(tt(),N) -> c_12(mark#(N))
            a__U51#(X1,X2,X3) -> c_13()
            a__U51#(tt(),M,N) -> c_14(a__U52#(a__isNat(N),M,N),a__isNat#(N))
            a__U52#(X1,X2,X3) -> c_15()
            a__U52#(tt(),M,N) -> c_16(a__plus#(mark(N),mark(M)),mark#(N),mark#(M))
            a__U61#(X) -> c_17()
            a__U61#(tt()) -> c_18()
            a__U71#(X1,X2,X3) -> c_19()
            a__U71#(tt(),M,N) -> c_20(a__U72#(a__isNat(N),M,N),a__isNat#(N))
            a__U72#(X1,X2,X3) -> c_21()
            a__U72#(tt(),M,N) -> c_22(a__plus#(a__x(mark(N),mark(M)),mark(N))
                                     ,a__x#(mark(N),mark(M))
                                     ,mark#(N)
                                     ,mark#(M)
                                     ,mark#(N))
            a__isNat#(X) -> c_23()
            a__isNat#(0()) -> c_24()
            a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1))
            a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1))
            a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1))
            a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N))
            a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M))
            a__plus#(X1,X2) -> c_30()
            a__x#(N,0()) -> c_31(a__U61#(a__isNat(N)),a__isNat#(N))
            a__x#(N,s(M)) -> c_32(a__U71#(a__isNat(M),M,N),a__isNat#(M))
            a__x#(X1,X2) -> c_33()
            mark#(0()) -> c_34()
            mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1))
            mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X))
            mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X))
            mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1))
            mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X))
            mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1))
            mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1))
            mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1))
            mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X))
            mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1))
            mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1))
            mark#(isNat(X)) -> c_46(a__isNat#(X))
            mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
            mark#(s(X)) -> c_48(mark#(X))
            mark#(tt()) -> c_49()
            mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
        - Weak TRS:
            a__U11(X1,X2) -> U11(X1,X2)
            a__U11(tt(),V2) -> a__U12(a__isNat(V2))
            a__U12(X) -> U12(X)
            a__U12(tt()) -> tt()
            a__U21(X) -> U21(X)
            a__U21(tt()) -> tt()
            a__U31(X1,X2) -> U31(X1,X2)
            a__U31(tt(),V2) -> a__U32(a__isNat(V2))
            a__U32(X) -> U32(X)
            a__U32(tt()) -> tt()
            a__U41(X1,X2) -> U41(X1,X2)
            a__U41(tt(),N) -> mark(N)
            a__U51(X1,X2,X3) -> U51(X1,X2,X3)
            a__U51(tt(),M,N) -> a__U52(a__isNat(N),M,N)
            a__U52(X1,X2,X3) -> U52(X1,X2,X3)
            a__U52(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
            a__U61(X) -> U61(X)
            a__U61(tt()) -> 0()
            a__U71(X1,X2,X3) -> U71(X1,X2,X3)
            a__U71(tt(),M,N) -> a__U72(a__isNat(N),M,N)
            a__U72(X1,X2,X3) -> U72(X1,X2,X3)
            a__U72(tt(),M,N) -> a__plus(a__x(mark(N),mark(M)),mark(N))
            a__isNat(X) -> isNat(X)
            a__isNat(0()) -> tt()
            a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
            a__isNat(s(V1)) -> a__U21(a__isNat(V1))
            a__isNat(x(V1,V2)) -> a__U31(a__isNat(V1),V2)
            a__plus(N,0()) -> a__U41(a__isNat(N),N)
            a__plus(N,s(M)) -> a__U51(a__isNat(M),M,N)
            a__plus(X1,X2) -> plus(X1,X2)
            a__x(N,0()) -> a__U61(a__isNat(N))
            a__x(N,s(M)) -> a__U71(a__isNat(M),M,N)
            a__x(X1,X2) -> x(X1,X2)
            mark(0()) -> 0()
            mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
            mark(U12(X)) -> a__U12(mark(X))
            mark(U21(X)) -> a__U21(mark(X))
            mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
            mark(U32(X)) -> a__U32(mark(X))
            mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
            mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
            mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
            mark(U61(X)) -> a__U61(mark(X))
            mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
            mark(U72(X1,X2,X3)) -> a__U72(mark(X1),X2,X3)
            mark(isNat(X)) -> a__isNat(X)
            mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
            mark(s(X)) -> s(mark(X))
            mark(tt()) -> tt()
            mark(x(X1,X2)) -> a__x(mark(X1),mark(X2))
        - Signature:
            {a__U11/2,a__U12/1,a__U21/1,a__U31/2,a__U32/1,a__U41/2,a__U51/3,a__U52/3,a__U61/1,a__U71/3,a__U72/3
            ,a__isNat/1,a__plus/2,a__x/2,mark/1,a__U11#/2,a__U12#/1,a__U21#/1,a__U31#/2,a__U32#/1,a__U41#/2,a__U51#/3
            ,a__U52#/3,a__U61#/1,a__U71#/3,a__U72#/3,a__isNat#/1,a__plus#/2,a__x#/2,mark#/1} / {0/0,U11/2,U12/1,U21/1
            ,U31/2,U32/1,U41/2,U51/3,U52/3,U61/1,U71/3,U72/3,isNat/1,plus/2,s/1,tt/0,x/2,c_1/0,c_2/2,c_3/0,c_4/0,c_5/0
            ,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/2,c_15/0,c_16/3,c_17/0,c_18/0,c_19/0,c_20/2,c_21/0
            ,c_22/5,c_23/0,c_24/0,c_25/2,c_26/2,c_27/2,c_28/2,c_29/2,c_30/0,c_31/2,c_32/2,c_33/0,c_34/0,c_35/2,c_36/2
            ,c_37/2,c_38/2,c_39/2,c_40/2,c_41/2,c_42/2,c_43/2,c_44/2,c_45/2,c_46/1,c_47/3,c_48/1,c_49/0,c_50/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__U11#,a__U12#,a__U21#,a__U31#,a__U32#,a__U41#,a__U51#
            ,a__U52#,a__U61#,a__U71#,a__U72#,a__isNat#,a__plus#,a__x#,mark#} and constructors {0,U11,U12,U21,U31,U32,U41
            ,U51,U52,U61,U71,U72,isNat,plus,s,tt,x}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,3,4,5,6,7,9,10,11,13,15,17,18,19,21,23,24,30,33,34,49}
        by application of
          Pre({1,3,4,5,6,7,9,10,11,13,15,17,18,19,21,23,24,30,33,34,49}) = {2,8,12,14,16,20,22,25,26,27,28,29,31,32
          ,35,36,37,38,39,40,41,42,43,44,45,46,47,48,50}.
        Here rules are labelled as follows:
          1: a__U11#(X1,X2) -> c_1()
          2: a__U11#(tt(),V2) -> c_2(a__U12#(a__isNat(V2)),a__isNat#(V2))
          3: a__U12#(X) -> c_3()
          4: a__U12#(tt()) -> c_4()
          5: a__U21#(X) -> c_5()
          6: a__U21#(tt()) -> c_6()
          7: a__U31#(X1,X2) -> c_7()
          8: a__U31#(tt(),V2) -> c_8(a__U32#(a__isNat(V2)),a__isNat#(V2))
          9: a__U32#(X) -> c_9()
          10: a__U32#(tt()) -> c_10()
          11: a__U41#(X1,X2) -> c_11()
          12: a__U41#(tt(),N) -> c_12(mark#(N))
          13: a__U51#(X1,X2,X3) -> c_13()
          14: a__U51#(tt(),M,N) -> c_14(a__U52#(a__isNat(N),M,N),a__isNat#(N))
          15: a__U52#(X1,X2,X3) -> c_15()
          16: a__U52#(tt(),M,N) -> c_16(a__plus#(mark(N),mark(M)),mark#(N),mark#(M))
          17: a__U61#(X) -> c_17()
          18: a__U61#(tt()) -> c_18()
          19: a__U71#(X1,X2,X3) -> c_19()
          20: a__U71#(tt(),M,N) -> c_20(a__U72#(a__isNat(N),M,N),a__isNat#(N))
          21: a__U72#(X1,X2,X3) -> c_21()
          22: a__U72#(tt(),M,N) -> c_22(a__plus#(a__x(mark(N),mark(M)),mark(N))
                                       ,a__x#(mark(N),mark(M))
                                       ,mark#(N)
                                       ,mark#(M)
                                       ,mark#(N))
          23: a__isNat#(X) -> c_23()
          24: a__isNat#(0()) -> c_24()
          25: a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1))
          26: a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1))
          27: a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1))
          28: a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N))
          29: a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M))
          30: a__plus#(X1,X2) -> c_30()
          31: a__x#(N,0()) -> c_31(a__U61#(a__isNat(N)),a__isNat#(N))
          32: a__x#(N,s(M)) -> c_32(a__U71#(a__isNat(M),M,N),a__isNat#(M))
          33: a__x#(X1,X2) -> c_33()
          34: mark#(0()) -> c_34()
          35: mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1))
          36: mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X))
          37: mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X))
          38: mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1))
          39: mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X))
          40: mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1))
          41: mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1))
          42: mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1))
          43: mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X))
          44: mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1))
          45: mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1))
          46: mark#(isNat(X)) -> c_46(a__isNat#(X))
          47: mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
          48: mark#(s(X)) -> c_48(mark#(X))
          49: mark#(tt()) -> c_49()
          50: mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
* Step 3: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            a__U11#(tt(),V2) -> c_2(a__U12#(a__isNat(V2)),a__isNat#(V2))
            a__U31#(tt(),V2) -> c_8(a__U32#(a__isNat(V2)),a__isNat#(V2))
            a__U41#(tt(),N) -> c_12(mark#(N))
            a__U51#(tt(),M,N) -> c_14(a__U52#(a__isNat(N),M,N),a__isNat#(N))
            a__U52#(tt(),M,N) -> c_16(a__plus#(mark(N),mark(M)),mark#(N),mark#(M))
            a__U71#(tt(),M,N) -> c_20(a__U72#(a__isNat(N),M,N),a__isNat#(N))
            a__U72#(tt(),M,N) -> c_22(a__plus#(a__x(mark(N),mark(M)),mark(N))
                                     ,a__x#(mark(N),mark(M))
                                     ,mark#(N)
                                     ,mark#(M)
                                     ,mark#(N))
            a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1))
            a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1))
            a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1))
            a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N))
            a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M))
            a__x#(N,0()) -> c_31(a__U61#(a__isNat(N)),a__isNat#(N))
            a__x#(N,s(M)) -> c_32(a__U71#(a__isNat(M),M,N),a__isNat#(M))
            mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1))
            mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X))
            mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X))
            mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1))
            mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X))
            mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1))
            mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1))
            mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1))
            mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X))
            mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1))
            mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1))
            mark#(isNat(X)) -> c_46(a__isNat#(X))
            mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
            mark#(s(X)) -> c_48(mark#(X))
            mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
        - Weak DPs:
            a__U11#(X1,X2) -> c_1()
            a__U12#(X) -> c_3()
            a__U12#(tt()) -> c_4()
            a__U21#(X) -> c_5()
            a__U21#(tt()) -> c_6()
            a__U31#(X1,X2) -> c_7()
            a__U32#(X) -> c_9()
            a__U32#(tt()) -> c_10()
            a__U41#(X1,X2) -> c_11()
            a__U51#(X1,X2,X3) -> c_13()
            a__U52#(X1,X2,X3) -> c_15()
            a__U61#(X) -> c_17()
            a__U61#(tt()) -> c_18()
            a__U71#(X1,X2,X3) -> c_19()
            a__U72#(X1,X2,X3) -> c_21()
            a__isNat#(X) -> c_23()
            a__isNat#(0()) -> c_24()
            a__plus#(X1,X2) -> c_30()
            a__x#(X1,X2) -> c_33()
            mark#(0()) -> c_34()
            mark#(tt()) -> c_49()
        - Weak TRS:
            a__U11(X1,X2) -> U11(X1,X2)
            a__U11(tt(),V2) -> a__U12(a__isNat(V2))
            a__U12(X) -> U12(X)
            a__U12(tt()) -> tt()
            a__U21(X) -> U21(X)
            a__U21(tt()) -> tt()
            a__U31(X1,X2) -> U31(X1,X2)
            a__U31(tt(),V2) -> a__U32(a__isNat(V2))
            a__U32(X) -> U32(X)
            a__U32(tt()) -> tt()
            a__U41(X1,X2) -> U41(X1,X2)
            a__U41(tt(),N) -> mark(N)
            a__U51(X1,X2,X3) -> U51(X1,X2,X3)
            a__U51(tt(),M,N) -> a__U52(a__isNat(N),M,N)
            a__U52(X1,X2,X3) -> U52(X1,X2,X3)
            a__U52(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
            a__U61(X) -> U61(X)
            a__U61(tt()) -> 0()
            a__U71(X1,X2,X3) -> U71(X1,X2,X3)
            a__U71(tt(),M,N) -> a__U72(a__isNat(N),M,N)
            a__U72(X1,X2,X3) -> U72(X1,X2,X3)
            a__U72(tt(),M,N) -> a__plus(a__x(mark(N),mark(M)),mark(N))
            a__isNat(X) -> isNat(X)
            a__isNat(0()) -> tt()
            a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
            a__isNat(s(V1)) -> a__U21(a__isNat(V1))
            a__isNat(x(V1,V2)) -> a__U31(a__isNat(V1),V2)
            a__plus(N,0()) -> a__U41(a__isNat(N),N)
            a__plus(N,s(M)) -> a__U51(a__isNat(M),M,N)
            a__plus(X1,X2) -> plus(X1,X2)
            a__x(N,0()) -> a__U61(a__isNat(N))
            a__x(N,s(M)) -> a__U71(a__isNat(M),M,N)
            a__x(X1,X2) -> x(X1,X2)
            mark(0()) -> 0()
            mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
            mark(U12(X)) -> a__U12(mark(X))
            mark(U21(X)) -> a__U21(mark(X))
            mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
            mark(U32(X)) -> a__U32(mark(X))
            mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
            mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
            mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
            mark(U61(X)) -> a__U61(mark(X))
            mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
            mark(U72(X1,X2,X3)) -> a__U72(mark(X1),X2,X3)
            mark(isNat(X)) -> a__isNat(X)
            mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
            mark(s(X)) -> s(mark(X))
            mark(tt()) -> tt()
            mark(x(X1,X2)) -> a__x(mark(X1),mark(X2))
        - Signature:
            {a__U11/2,a__U12/1,a__U21/1,a__U31/2,a__U32/1,a__U41/2,a__U51/3,a__U52/3,a__U61/1,a__U71/3,a__U72/3
            ,a__isNat/1,a__plus/2,a__x/2,mark/1,a__U11#/2,a__U12#/1,a__U21#/1,a__U31#/2,a__U32#/1,a__U41#/2,a__U51#/3
            ,a__U52#/3,a__U61#/1,a__U71#/3,a__U72#/3,a__isNat#/1,a__plus#/2,a__x#/2,mark#/1} / {0/0,U11/2,U12/1,U21/1
            ,U31/2,U32/1,U41/2,U51/3,U52/3,U61/1,U71/3,U72/3,isNat/1,plus/2,s/1,tt/0,x/2,c_1/0,c_2/2,c_3/0,c_4/0,c_5/0
            ,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/2,c_15/0,c_16/3,c_17/0,c_18/0,c_19/0,c_20/2,c_21/0
            ,c_22/5,c_23/0,c_24/0,c_25/2,c_26/2,c_27/2,c_28/2,c_29/2,c_30/0,c_31/2,c_32/2,c_33/0,c_34/0,c_35/2,c_36/2
            ,c_37/2,c_38/2,c_39/2,c_40/2,c_41/2,c_42/2,c_43/2,c_44/2,c_45/2,c_46/1,c_47/3,c_48/1,c_49/0,c_50/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__U11#,a__U12#,a__U21#,a__U31#,a__U32#,a__U41#,a__U51#
            ,a__U52#,a__U61#,a__U71#,a__U72#,a__isNat#,a__plus#,a__x#,mark#} and constructors {0,U11,U12,U21,U31,U32,U41
            ,U51,U52,U61,U71,U72,isNat,plus,s,tt,x}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:a__U11#(tt(),V2) -> c_2(a__U12#(a__isNat(V2)),a__isNat#(V2))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_2 a__isNat#(0()) -> c_24():46
             -->_2 a__isNat#(X) -> c_23():45
             -->_1 a__U12#(tt()) -> c_4():32
             -->_1 a__U12#(X) -> c_3():31
          
          2:S:a__U31#(tt(),V2) -> c_8(a__U32#(a__isNat(V2)),a__isNat#(V2))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_2 a__isNat#(0()) -> c_24():46
             -->_2 a__isNat#(X) -> c_23():45
             -->_1 a__U32#(tt()) -> c_10():37
             -->_1 a__U32#(X) -> c_9():36
          
          3:S:a__U41#(tt(),N) -> c_12(mark#(N))
             -->_1 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_1 mark#(s(X)) -> c_48(mark#(X)):28
             -->_1 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_1 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_1 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_1 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_1 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_1 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_1 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_1 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_1 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_1 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_1 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_1 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_1 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 mark#(tt()) -> c_49():50
             -->_1 mark#(0()) -> c_34():49
          
          4:S:a__U51#(tt(),M,N) -> c_14(a__U52#(a__isNat(N),M,N),a__isNat#(N))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U52#(tt(),M,N) -> c_16(a__plus#(mark(N),mark(M)),mark#(N),mark#(M)):5
             -->_2 a__isNat#(0()) -> c_24():46
             -->_2 a__isNat#(X) -> c_23():45
             -->_1 a__U52#(X1,X2,X3) -> c_15():40
          
          5:S:a__U52#(tt(),M,N) -> c_16(a__plus#(mark(N),mark(M)),mark#(N),mark#(M))
             -->_3 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_3 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_3 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_3 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_3 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_3 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_3 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_3 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_3 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_3 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_3 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_3 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_3 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_3 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_3 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M)):12
             -->_1 a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N)):11
             -->_3 mark#(tt()) -> c_49():50
             -->_2 mark#(tt()) -> c_49():50
             -->_3 mark#(0()) -> c_34():49
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__plus#(X1,X2) -> c_30():47
          
          6:S:a__U71#(tt(),M,N) -> c_20(a__U72#(a__isNat(N),M,N),a__isNat#(N))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U72#(tt(),M,N) -> c_22(a__plus#(a__x(mark(N),mark(M)),mark(N))
                                            ,a__x#(mark(N),mark(M))
                                            ,mark#(N)
                                            ,mark#(M)
                                            ,mark#(N)):7
             -->_2 a__isNat#(0()) -> c_24():46
             -->_2 a__isNat#(X) -> c_23():45
             -->_1 a__U72#(X1,X2,X3) -> c_21():44
          
          7:S:a__U72#(tt(),M,N) -> c_22(a__plus#(a__x(mark(N),mark(M)),mark(N))
                                       ,a__x#(mark(N),mark(M))
                                       ,mark#(N)
                                       ,mark#(M)
                                       ,mark#(N))
             -->_5 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_4 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_3 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_5 mark#(s(X)) -> c_48(mark#(X)):28
             -->_4 mark#(s(X)) -> c_48(mark#(X)):28
             -->_3 mark#(s(X)) -> c_48(mark#(X)):28
             -->_5 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_4 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_3 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_5 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_4 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_3 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_5 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_4 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_3 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_5 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_4 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_3 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_5 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_4 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_3 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_5 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_4 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_3 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_5 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_4 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_3 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_5 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_4 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_3 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_5 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_4 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_3 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_5 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_4 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_3 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_5 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_4 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_3 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_5 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_4 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_3 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_5 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_4 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_3 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_2 a__x#(N,s(M)) -> c_32(a__U71#(a__isNat(M),M,N),a__isNat#(M)):14
             -->_2 a__x#(N,0()) -> c_31(a__U61#(a__isNat(N)),a__isNat#(N)):13
             -->_1 a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M)):12
             -->_1 a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N)):11
             -->_5 mark#(tt()) -> c_49():50
             -->_4 mark#(tt()) -> c_49():50
             -->_3 mark#(tt()) -> c_49():50
             -->_5 mark#(0()) -> c_34():49
             -->_4 mark#(0()) -> c_34():49
             -->_3 mark#(0()) -> c_34():49
             -->_2 a__x#(X1,X2) -> c_33():48
             -->_1 a__plus#(X1,X2) -> c_30():47
          
          8:S:a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(0()) -> c_24():46
             -->_2 a__isNat#(X) -> c_23():45
             -->_1 a__U11#(X1,X2) -> c_1():30
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U11#(tt(),V2) -> c_2(a__U12#(a__isNat(V2)),a__isNat#(V2)):1
          
          9:S:a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(0()) -> c_24():46
             -->_2 a__isNat#(X) -> c_23():45
             -->_1 a__U21#(tt()) -> c_6():34
             -->_1 a__U21#(X) -> c_5():33
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
          
          10:S:a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1))
             -->_2 a__isNat#(0()) -> c_24():46
             -->_2 a__isNat#(X) -> c_23():45
             -->_1 a__U31#(X1,X2) -> c_7():35
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U31#(tt(),V2) -> c_8(a__U32#(a__isNat(V2)),a__isNat#(V2)):2
          
          11:S:a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N))
             -->_2 a__isNat#(0()) -> c_24():46
             -->_2 a__isNat#(X) -> c_23():45
             -->_1 a__U41#(X1,X2) -> c_11():38
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U41#(tt(),N) -> c_12(mark#(N)):3
          
          12:S:a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M))
             -->_2 a__isNat#(0()) -> c_24():46
             -->_2 a__isNat#(X) -> c_23():45
             -->_1 a__U51#(X1,X2,X3) -> c_13():39
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U51#(tt(),M,N) -> c_14(a__U52#(a__isNat(N),M,N),a__isNat#(N)):4
          
          13:S:a__x#(N,0()) -> c_31(a__U61#(a__isNat(N)),a__isNat#(N))
             -->_2 a__isNat#(0()) -> c_24():46
             -->_2 a__isNat#(X) -> c_23():45
             -->_1 a__U61#(tt()) -> c_18():42
             -->_1 a__U61#(X) -> c_17():41
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
          
          14:S:a__x#(N,s(M)) -> c_32(a__U71#(a__isNat(M),M,N),a__isNat#(M))
             -->_2 a__isNat#(0()) -> c_24():46
             -->_2 a__isNat#(X) -> c_23():45
             -->_1 a__U71#(X1,X2,X3) -> c_19():43
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U71#(tt(),M,N) -> c_20(a__U72#(a__isNat(N),M,N),a__isNat#(N)):6
          
          15:S:mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(tt()) -> c_49():50
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__U11#(X1,X2) -> c_1():30
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U11#(tt(),V2) -> c_2(a__U12#(a__isNat(V2)),a__isNat#(V2)):1
          
          16:S:mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(tt()) -> c_49():50
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__U12#(tt()) -> c_4():32
             -->_1 a__U12#(X) -> c_3():31
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
          
          17:S:mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(tt()) -> c_49():50
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__U21#(tt()) -> c_6():34
             -->_1 a__U21#(X) -> c_5():33
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
          
          18:S:mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(tt()) -> c_49():50
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__U31#(X1,X2) -> c_7():35
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U31#(tt(),V2) -> c_8(a__U32#(a__isNat(V2)),a__isNat#(V2)):2
          
          19:S:mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(tt()) -> c_49():50
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__U32#(tt()) -> c_10():37
             -->_1 a__U32#(X) -> c_9():36
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
          
          20:S:mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(tt()) -> c_49():50
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__U41#(X1,X2) -> c_11():38
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U41#(tt(),N) -> c_12(mark#(N)):3
          
          21:S:mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(tt()) -> c_49():50
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__U51#(X1,X2,X3) -> c_13():39
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U51#(tt(),M,N) -> c_14(a__U52#(a__isNat(N),M,N),a__isNat#(N)):4
          
          22:S:mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(tt()) -> c_49():50
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__U52#(X1,X2,X3) -> c_15():40
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U52#(tt(),M,N) -> c_16(a__plus#(mark(N),mark(M)),mark#(N),mark#(M)):5
          
          23:S:mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(tt()) -> c_49():50
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__U61#(tt()) -> c_18():42
             -->_1 a__U61#(X) -> c_17():41
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
          
          24:S:mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(tt()) -> c_49():50
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__U71#(X1,X2,X3) -> c_19():43
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U71#(tt(),M,N) -> c_20(a__U72#(a__isNat(N),M,N),a__isNat#(N)):6
          
          25:S:mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(tt()) -> c_49():50
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__U72#(X1,X2,X3) -> c_21():44
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U72#(tt(),M,N) -> c_22(a__plus#(a__x(mark(N),mark(M)),mark(N))
                                            ,a__x#(mark(N),mark(M))
                                            ,mark#(N)
                                            ,mark#(M)
                                            ,mark#(N)):7
          
          26:S:mark#(isNat(X)) -> c_46(a__isNat#(X))
             -->_1 a__isNat#(0()) -> c_24():46
             -->_1 a__isNat#(X) -> c_23():45
             -->_1 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_1 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_1 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
          
          27:S:mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
             -->_3 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_3 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_3 mark#(tt()) -> c_49():50
             -->_2 mark#(tt()) -> c_49():50
             -->_3 mark#(0()) -> c_34():49
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__plus#(X1,X2) -> c_30():47
             -->_3 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_3 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_3 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_3 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_3 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_3 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_3 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_3 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_3 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_3 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_3 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_3 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_3 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M)):12
             -->_1 a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N)):11
          
          28:S:mark#(s(X)) -> c_48(mark#(X))
             -->_1 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_1 mark#(tt()) -> c_49():50
             -->_1 mark#(0()) -> c_34():49
             -->_1 mark#(s(X)) -> c_48(mark#(X)):28
             -->_1 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_1 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_1 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_1 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_1 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_1 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_1 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_1 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_1 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_1 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_1 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_1 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_1 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
          
          29:S:mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
             -->_3 mark#(tt()) -> c_49():50
             -->_2 mark#(tt()) -> c_49():50
             -->_3 mark#(0()) -> c_34():49
             -->_2 mark#(0()) -> c_34():49
             -->_1 a__x#(X1,X2) -> c_33():48
             -->_3 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_3 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_3 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_3 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_3 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_3 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_3 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_3 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_3 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_3 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_3 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_3 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_3 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_3 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_3 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__x#(N,s(M)) -> c_32(a__U71#(a__isNat(M),M,N),a__isNat#(M)):14
             -->_1 a__x#(N,0()) -> c_31(a__U61#(a__isNat(N)),a__isNat#(N)):13
          
          30:W:a__U11#(X1,X2) -> c_1()
             
          
          31:W:a__U12#(X) -> c_3()
             
          
          32:W:a__U12#(tt()) -> c_4()
             
          
          33:W:a__U21#(X) -> c_5()
             
          
          34:W:a__U21#(tt()) -> c_6()
             
          
          35:W:a__U31#(X1,X2) -> c_7()
             
          
          36:W:a__U32#(X) -> c_9()
             
          
          37:W:a__U32#(tt()) -> c_10()
             
          
          38:W:a__U41#(X1,X2) -> c_11()
             
          
          39:W:a__U51#(X1,X2,X3) -> c_13()
             
          
          40:W:a__U52#(X1,X2,X3) -> c_15()
             
          
          41:W:a__U61#(X) -> c_17()
             
          
          42:W:a__U61#(tt()) -> c_18()
             
          
          43:W:a__U71#(X1,X2,X3) -> c_19()
             
          
          44:W:a__U72#(X1,X2,X3) -> c_21()
             
          
          45:W:a__isNat#(X) -> c_23()
             
          
          46:W:a__isNat#(0()) -> c_24()
             
          
          47:W:a__plus#(X1,X2) -> c_30()
             
          
          48:W:a__x#(X1,X2) -> c_33()
             
          
          49:W:mark#(0()) -> c_34()
             
          
          50:W:mark#(tt()) -> c_49()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          38: a__U41#(X1,X2) -> c_11()
          39: a__U51#(X1,X2,X3) -> c_13()
          40: a__U52#(X1,X2,X3) -> c_15()
          41: a__U61#(X) -> c_17()
          42: a__U61#(tt()) -> c_18()
          43: a__U71#(X1,X2,X3) -> c_19()
          44: a__U72#(X1,X2,X3) -> c_21()
          47: a__plus#(X1,X2) -> c_30()
          48: a__x#(X1,X2) -> c_33()
          49: mark#(0()) -> c_34()
          50: mark#(tt()) -> c_49()
          31: a__U12#(X) -> c_3()
          32: a__U12#(tt()) -> c_4()
          36: a__U32#(X) -> c_9()
          37: a__U32#(tt()) -> c_10()
          30: a__U11#(X1,X2) -> c_1()
          33: a__U21#(X) -> c_5()
          34: a__U21#(tt()) -> c_6()
          35: a__U31#(X1,X2) -> c_7()
          45: a__isNat#(X) -> c_23()
          46: a__isNat#(0()) -> c_24()
* Step 4: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            a__U11#(tt(),V2) -> c_2(a__U12#(a__isNat(V2)),a__isNat#(V2))
            a__U31#(tt(),V2) -> c_8(a__U32#(a__isNat(V2)),a__isNat#(V2))
            a__U41#(tt(),N) -> c_12(mark#(N))
            a__U51#(tt(),M,N) -> c_14(a__U52#(a__isNat(N),M,N),a__isNat#(N))
            a__U52#(tt(),M,N) -> c_16(a__plus#(mark(N),mark(M)),mark#(N),mark#(M))
            a__U71#(tt(),M,N) -> c_20(a__U72#(a__isNat(N),M,N),a__isNat#(N))
            a__U72#(tt(),M,N) -> c_22(a__plus#(a__x(mark(N),mark(M)),mark(N))
                                     ,a__x#(mark(N),mark(M))
                                     ,mark#(N)
                                     ,mark#(M)
                                     ,mark#(N))
            a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1))
            a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1))
            a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1))
            a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N))
            a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M))
            a__x#(N,0()) -> c_31(a__U61#(a__isNat(N)),a__isNat#(N))
            a__x#(N,s(M)) -> c_32(a__U71#(a__isNat(M),M,N),a__isNat#(M))
            mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1))
            mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X))
            mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X))
            mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1))
            mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X))
            mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1))
            mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1))
            mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1))
            mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X))
            mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1))
            mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1))
            mark#(isNat(X)) -> c_46(a__isNat#(X))
            mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
            mark#(s(X)) -> c_48(mark#(X))
            mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
        - Weak TRS:
            a__U11(X1,X2) -> U11(X1,X2)
            a__U11(tt(),V2) -> a__U12(a__isNat(V2))
            a__U12(X) -> U12(X)
            a__U12(tt()) -> tt()
            a__U21(X) -> U21(X)
            a__U21(tt()) -> tt()
            a__U31(X1,X2) -> U31(X1,X2)
            a__U31(tt(),V2) -> a__U32(a__isNat(V2))
            a__U32(X) -> U32(X)
            a__U32(tt()) -> tt()
            a__U41(X1,X2) -> U41(X1,X2)
            a__U41(tt(),N) -> mark(N)
            a__U51(X1,X2,X3) -> U51(X1,X2,X3)
            a__U51(tt(),M,N) -> a__U52(a__isNat(N),M,N)
            a__U52(X1,X2,X3) -> U52(X1,X2,X3)
            a__U52(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
            a__U61(X) -> U61(X)
            a__U61(tt()) -> 0()
            a__U71(X1,X2,X3) -> U71(X1,X2,X3)
            a__U71(tt(),M,N) -> a__U72(a__isNat(N),M,N)
            a__U72(X1,X2,X3) -> U72(X1,X2,X3)
            a__U72(tt(),M,N) -> a__plus(a__x(mark(N),mark(M)),mark(N))
            a__isNat(X) -> isNat(X)
            a__isNat(0()) -> tt()
            a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
            a__isNat(s(V1)) -> a__U21(a__isNat(V1))
            a__isNat(x(V1,V2)) -> a__U31(a__isNat(V1),V2)
            a__plus(N,0()) -> a__U41(a__isNat(N),N)
            a__plus(N,s(M)) -> a__U51(a__isNat(M),M,N)
            a__plus(X1,X2) -> plus(X1,X2)
            a__x(N,0()) -> a__U61(a__isNat(N))
            a__x(N,s(M)) -> a__U71(a__isNat(M),M,N)
            a__x(X1,X2) -> x(X1,X2)
            mark(0()) -> 0()
            mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
            mark(U12(X)) -> a__U12(mark(X))
            mark(U21(X)) -> a__U21(mark(X))
            mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
            mark(U32(X)) -> a__U32(mark(X))
            mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
            mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
            mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
            mark(U61(X)) -> a__U61(mark(X))
            mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
            mark(U72(X1,X2,X3)) -> a__U72(mark(X1),X2,X3)
            mark(isNat(X)) -> a__isNat(X)
            mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
            mark(s(X)) -> s(mark(X))
            mark(tt()) -> tt()
            mark(x(X1,X2)) -> a__x(mark(X1),mark(X2))
        - Signature:
            {a__U11/2,a__U12/1,a__U21/1,a__U31/2,a__U32/1,a__U41/2,a__U51/3,a__U52/3,a__U61/1,a__U71/3,a__U72/3
            ,a__isNat/1,a__plus/2,a__x/2,mark/1,a__U11#/2,a__U12#/1,a__U21#/1,a__U31#/2,a__U32#/1,a__U41#/2,a__U51#/3
            ,a__U52#/3,a__U61#/1,a__U71#/3,a__U72#/3,a__isNat#/1,a__plus#/2,a__x#/2,mark#/1} / {0/0,U11/2,U12/1,U21/1
            ,U31/2,U32/1,U41/2,U51/3,U52/3,U61/1,U71/3,U72/3,isNat/1,plus/2,s/1,tt/0,x/2,c_1/0,c_2/2,c_3/0,c_4/0,c_5/0
            ,c_6/0,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/2,c_15/0,c_16/3,c_17/0,c_18/0,c_19/0,c_20/2,c_21/0
            ,c_22/5,c_23/0,c_24/0,c_25/2,c_26/2,c_27/2,c_28/2,c_29/2,c_30/0,c_31/2,c_32/2,c_33/0,c_34/0,c_35/2,c_36/2
            ,c_37/2,c_38/2,c_39/2,c_40/2,c_41/2,c_42/2,c_43/2,c_44/2,c_45/2,c_46/1,c_47/3,c_48/1,c_49/0,c_50/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__U11#,a__U12#,a__U21#,a__U31#,a__U32#,a__U41#,a__U51#
            ,a__U52#,a__U61#,a__U71#,a__U72#,a__isNat#,a__plus#,a__x#,mark#} and constructors {0,U11,U12,U21,U31,U32,U41
            ,U51,U52,U61,U71,U72,isNat,plus,s,tt,x}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:a__U11#(tt(),V2) -> c_2(a__U12#(a__isNat(V2)),a__isNat#(V2))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
          
          2:S:a__U31#(tt(),V2) -> c_8(a__U32#(a__isNat(V2)),a__isNat#(V2))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
          
          3:S:a__U41#(tt(),N) -> c_12(mark#(N))
             -->_1 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_1 mark#(s(X)) -> c_48(mark#(X)):28
             -->_1 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_1 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_1 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_1 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_1 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_1 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_1 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_1 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_1 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_1 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_1 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_1 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_1 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
          
          4:S:a__U51#(tt(),M,N) -> c_14(a__U52#(a__isNat(N),M,N),a__isNat#(N))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U52#(tt(),M,N) -> c_16(a__plus#(mark(N),mark(M)),mark#(N),mark#(M)):5
          
          5:S:a__U52#(tt(),M,N) -> c_16(a__plus#(mark(N),mark(M)),mark#(N),mark#(M))
             -->_3 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_3 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_3 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_3 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_3 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_3 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_3 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_3 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_3 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_3 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_3 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_3 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_3 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_3 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_3 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M)):12
             -->_1 a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N)):11
          
          6:S:a__U71#(tt(),M,N) -> c_20(a__U72#(a__isNat(N),M,N),a__isNat#(N))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U72#(tt(),M,N) -> c_22(a__plus#(a__x(mark(N),mark(M)),mark(N))
                                            ,a__x#(mark(N),mark(M))
                                            ,mark#(N)
                                            ,mark#(M)
                                            ,mark#(N)):7
          
          7:S:a__U72#(tt(),M,N) -> c_22(a__plus#(a__x(mark(N),mark(M)),mark(N))
                                       ,a__x#(mark(N),mark(M))
                                       ,mark#(N)
                                       ,mark#(M)
                                       ,mark#(N))
             -->_5 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_4 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_3 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_5 mark#(s(X)) -> c_48(mark#(X)):28
             -->_4 mark#(s(X)) -> c_48(mark#(X)):28
             -->_3 mark#(s(X)) -> c_48(mark#(X)):28
             -->_5 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_4 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_3 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_5 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_4 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_3 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_5 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_4 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_3 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_5 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_4 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_3 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_5 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_4 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_3 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_5 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_4 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_3 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_5 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_4 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_3 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_5 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_4 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_3 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_5 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_4 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_3 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_5 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_4 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_3 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_5 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_4 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_3 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_5 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_4 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_3 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_5 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_4 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_3 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_2 a__x#(N,s(M)) -> c_32(a__U71#(a__isNat(M),M,N),a__isNat#(M)):14
             -->_2 a__x#(N,0()) -> c_31(a__U61#(a__isNat(N)),a__isNat#(N)):13
             -->_1 a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M)):12
             -->_1 a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N)):11
          
          8:S:a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U11#(tt(),V2) -> c_2(a__U12#(a__isNat(V2)),a__isNat#(V2)):1
          
          9:S:a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
          
          10:S:a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U31#(tt(),V2) -> c_8(a__U32#(a__isNat(V2)),a__isNat#(V2)):2
          
          11:S:a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U41#(tt(),N) -> c_12(mark#(N)):3
          
          12:S:a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U51#(tt(),M,N) -> c_14(a__U52#(a__isNat(N),M,N),a__isNat#(N)):4
          
          13:S:a__x#(N,0()) -> c_31(a__U61#(a__isNat(N)),a__isNat#(N))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
          
          14:S:a__x#(N,s(M)) -> c_32(a__U71#(a__isNat(M),M,N),a__isNat#(M))
             -->_2 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_2 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_2 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
             -->_1 a__U71#(tt(),M,N) -> c_20(a__U72#(a__isNat(N),M,N),a__isNat#(N)):6
          
          15:S:mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U11#(tt(),V2) -> c_2(a__U12#(a__isNat(V2)),a__isNat#(V2)):1
          
          16:S:mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
          
          17:S:mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
          
          18:S:mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U31#(tt(),V2) -> c_8(a__U32#(a__isNat(V2)),a__isNat#(V2)):2
          
          19:S:mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
          
          20:S:mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U41#(tt(),N) -> c_12(mark#(N)):3
          
          21:S:mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U51#(tt(),M,N) -> c_14(a__U52#(a__isNat(N),M,N),a__isNat#(N)):4
          
          22:S:mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U52#(tt(),M,N) -> c_16(a__plus#(mark(N),mark(M)),mark#(N),mark#(M)):5
          
          23:S:mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
          
          24:S:mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U71#(tt(),M,N) -> c_20(a__U72#(a__isNat(N),M,N),a__isNat#(N)):6
          
          25:S:mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1))
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__U72#(tt(),M,N) -> c_22(a__plus#(a__x(mark(N),mark(M)),mark(N))
                                            ,a__x#(mark(N),mark(M))
                                            ,mark#(N)
                                            ,mark#(M)
                                            ,mark#(N)):7
          
          26:S:mark#(isNat(X)) -> c_46(a__isNat#(X))
             -->_1 a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1)):10
             -->_1 a__isNat#(s(V1)) -> c_26(a__U21#(a__isNat(V1)),a__isNat#(V1)):9
             -->_1 a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1)):8
          
          27:S:mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
             -->_3 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_3 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_3 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_3 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_3 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_3 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_3 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_3 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_3 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_3 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_3 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_3 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_3 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_3 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_3 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M)):12
             -->_1 a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N)):11
          
          28:S:mark#(s(X)) -> c_48(mark#(X))
             -->_1 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_1 mark#(s(X)) -> c_48(mark#(X)):28
             -->_1 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_1 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_1 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_1 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_1 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_1 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_1 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_1 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_1 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_1 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_1 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_1 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_1 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
          
          29:S:mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
             -->_3 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_2 mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):29
             -->_3 mark#(s(X)) -> c_48(mark#(X)):28
             -->_2 mark#(s(X)) -> c_48(mark#(X)):28
             -->_3 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_2 mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):27
             -->_3 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_2 mark#(isNat(X)) -> c_46(a__isNat#(X)):26
             -->_3 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_2 mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1)):25
             -->_3 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_2 mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1)):24
             -->_3 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_2 mark#(U61(X)) -> c_43(a__U61#(mark(X)),mark#(X)):23
             -->_3 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_2 mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1)):22
             -->_3 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_2 mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1)):21
             -->_3 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_2 mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1)):20
             -->_3 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_2 mark#(U32(X)) -> c_39(a__U32#(mark(X)),mark#(X)):19
             -->_3 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_2 mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1)):18
             -->_3 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_2 mark#(U21(X)) -> c_37(a__U21#(mark(X)),mark#(X)):17
             -->_3 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_2 mark#(U12(X)) -> c_36(a__U12#(mark(X)),mark#(X)):16
             -->_3 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_2 mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1)):15
             -->_1 a__x#(N,s(M)) -> c_32(a__U71#(a__isNat(M),M,N),a__isNat#(M)):14
             -->_1 a__x#(N,0()) -> c_31(a__U61#(a__isNat(N)),a__isNat#(N)):13
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          a__U11#(tt(),V2) -> c_2(a__isNat#(V2))
          a__U31#(tt(),V2) -> c_8(a__isNat#(V2))
          a__isNat#(s(V1)) -> c_26(a__isNat#(V1))
          a__x#(N,0()) -> c_31(a__isNat#(N))
          mark#(U12(X)) -> c_36(mark#(X))
          mark#(U21(X)) -> c_37(mark#(X))
          mark#(U32(X)) -> c_39(mark#(X))
          mark#(U61(X)) -> c_43(mark#(X))
* Step 5: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          a__U11#(tt(),V2) -> c_2(a__isNat#(V2))
          a__U31#(tt(),V2) -> c_8(a__isNat#(V2))
          a__U41#(tt(),N) -> c_12(mark#(N))
          a__U51#(tt(),M,N) -> c_14(a__U52#(a__isNat(N),M,N),a__isNat#(N))
          a__U52#(tt(),M,N) -> c_16(a__plus#(mark(N),mark(M)),mark#(N),mark#(M))
          a__U71#(tt(),M,N) -> c_20(a__U72#(a__isNat(N),M,N),a__isNat#(N))
          a__U72#(tt(),M,N) -> c_22(a__plus#(a__x(mark(N),mark(M)),mark(N))
                                   ,a__x#(mark(N),mark(M))
                                   ,mark#(N)
                                   ,mark#(M)
                                   ,mark#(N))
          a__isNat#(plus(V1,V2)) -> c_25(a__U11#(a__isNat(V1),V2),a__isNat#(V1))
          a__isNat#(s(V1)) -> c_26(a__isNat#(V1))
          a__isNat#(x(V1,V2)) -> c_27(a__U31#(a__isNat(V1),V2),a__isNat#(V1))
          a__plus#(N,0()) -> c_28(a__U41#(a__isNat(N),N),a__isNat#(N))
          a__plus#(N,s(M)) -> c_29(a__U51#(a__isNat(M),M,N),a__isNat#(M))
          a__x#(N,0()) -> c_31(a__isNat#(N))
          a__x#(N,s(M)) -> c_32(a__U71#(a__isNat(M),M,N),a__isNat#(M))
          mark#(U11(X1,X2)) -> c_35(a__U11#(mark(X1),X2),mark#(X1))
          mark#(U12(X)) -> c_36(mark#(X))
          mark#(U21(X)) -> c_37(mark#(X))
          mark#(U31(X1,X2)) -> c_38(a__U31#(mark(X1),X2),mark#(X1))
          mark#(U32(X)) -> c_39(mark#(X))
          mark#(U41(X1,X2)) -> c_40(a__U41#(mark(X1),X2),mark#(X1))
          mark#(U51(X1,X2,X3)) -> c_41(a__U51#(mark(X1),X2,X3),mark#(X1))
          mark#(U52(X1,X2,X3)) -> c_42(a__U52#(mark(X1),X2,X3),mark#(X1))
          mark#(U61(X)) -> c_43(mark#(X))
          mark#(U71(X1,X2,X3)) -> c_44(a__U71#(mark(X1),X2,X3),mark#(X1))
          mark#(U72(X1,X2,X3)) -> c_45(a__U72#(mark(X1),X2,X3),mark#(X1))
          mark#(isNat(X)) -> c_46(a__isNat#(X))
          mark#(plus(X1,X2)) -> c_47(a__plus#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
          mark#(s(X)) -> c_48(mark#(X))
          mark#(x(X1,X2)) -> c_50(a__x#(mark(X1),mark(X2)),mark#(X1),mark#(X2))
      - Weak TRS:
          a__U11(X1,X2) -> U11(X1,X2)
          a__U11(tt(),V2) -> a__U12(a__isNat(V2))
          a__U12(X) -> U12(X)
          a__U12(tt()) -> tt()
          a__U21(X) -> U21(X)
          a__U21(tt()) -> tt()
          a__U31(X1,X2) -> U31(X1,X2)
          a__U31(tt(),V2) -> a__U32(a__isNat(V2))
          a__U32(X) -> U32(X)
          a__U32(tt()) -> tt()
          a__U41(X1,X2) -> U41(X1,X2)
          a__U41(tt(),N) -> mark(N)
          a__U51(X1,X2,X3) -> U51(X1,X2,X3)
          a__U51(tt(),M,N) -> a__U52(a__isNat(N),M,N)
          a__U52(X1,X2,X3) -> U52(X1,X2,X3)
          a__U52(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
          a__U61(X) -> U61(X)
          a__U61(tt()) -> 0()
          a__U71(X1,X2,X3) -> U71(X1,X2,X3)
          a__U71(tt(),M,N) -> a__U72(a__isNat(N),M,N)
          a__U72(X1,X2,X3) -> U72(X1,X2,X3)
          a__U72(tt(),M,N) -> a__plus(a__x(mark(N),mark(M)),mark(N))
          a__isNat(X) -> isNat(X)
          a__isNat(0()) -> tt()
          a__isNat(plus(V1,V2)) -> a__U11(a__isNat(V1),V2)
          a__isNat(s(V1)) -> a__U21(a__isNat(V1))
          a__isNat(x(V1,V2)) -> a__U31(a__isNat(V1),V2)
          a__plus(N,0()) -> a__U41(a__isNat(N),N)
          a__plus(N,s(M)) -> a__U51(a__isNat(M),M,N)
          a__plus(X1,X2) -> plus(X1,X2)
          a__x(N,0()) -> a__U61(a__isNat(N))
          a__x(N,s(M)) -> a__U71(a__isNat(M),M,N)
          a__x(X1,X2) -> x(X1,X2)
          mark(0()) -> 0()
          mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
          mark(U12(X)) -> a__U12(mark(X))
          mark(U21(X)) -> a__U21(mark(X))
          mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
          mark(U32(X)) -> a__U32(mark(X))
          mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
          mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
          mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
          mark(U61(X)) -> a__U61(mark(X))
          mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
          mark(U72(X1,X2,X3)) -> a__U72(mark(X1),X2,X3)
          mark(isNat(X)) -> a__isNat(X)
          mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
          mark(s(X)) -> s(mark(X))
          mark(tt()) -> tt()
          mark(x(X1,X2)) -> a__x(mark(X1),mark(X2))
      - Signature:
          {a__U11/2,a__U12/1,a__U21/1,a__U31/2,a__U32/1,a__U41/2,a__U51/3,a__U52/3,a__U61/1,a__U71/3,a__U72/3
          ,a__isNat/1,a__plus/2,a__x/2,mark/1,a__U11#/2,a__U12#/1,a__U21#/1,a__U31#/2,a__U32#/1,a__U41#/2,a__U51#/3
          ,a__U52#/3,a__U61#/1,a__U71#/3,a__U72#/3,a__isNat#/1,a__plus#/2,a__x#/2,mark#/1} / {0/0,U11/2,U12/1,U21/1
          ,U31/2,U32/1,U41/2,U51/3,U52/3,U61/1,U71/3,U72/3,isNat/1,plus/2,s/1,tt/0,x/2,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0
          ,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/2,c_15/0,c_16/3,c_17/0,c_18/0,c_19/0,c_20/2,c_21/0
          ,c_22/5,c_23/0,c_24/0,c_25/2,c_26/1,c_27/2,c_28/2,c_29/2,c_30/0,c_31/1,c_32/2,c_33/0,c_34/0,c_35/2,c_36/1
          ,c_37/1,c_38/2,c_39/1,c_40/2,c_41/2,c_42/2,c_43/1,c_44/2,c_45/2,c_46/1,c_47/3,c_48/1,c_49/0,c_50/3}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {a__U11#,a__U12#,a__U21#,a__U31#,a__U32#,a__U41#,a__U51#
          ,a__U52#,a__U61#,a__U71#,a__U72#,a__isNat#,a__plus#,a__x#,mark#} and constructors {0,U11,U12,U21,U31,U32,U41
          ,U51,U52,U61,U71,U72,isNat,plus,s,tt,x}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE