Problem Transformed CSR 04 MYNAT complete Z

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 MYNAT complete Z

stdout:

MAYBE

Problem:
U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
U12(tt(),V2) -> U13(isNat(activate(V2)))
U13(tt()) -> tt()
U21(tt(),V1) -> U22(isNat(activate(V1)))
U22(tt()) -> tt()
U31(tt(),V1,V2) -> U32(isNat(activate(V1)),activate(V2))
U32(tt(),V2) -> U33(isNat(activate(V2)))
U33(tt()) -> tt()
U41(tt(),N) -> activate(N)
U51(tt(),M,N) -> s(plus(activate(N),activate(M)))
U61(tt()) -> 0()
U71(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
and(tt(),X) -> activate(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) ->
U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNat(n__x(V1,V2)) ->
U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
isNatKind(n__s(V1)) -> isNatKind(activate(V1))
isNatKind(n__x(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
plus(N,0()) -> U41(and(isNat(N),n__isNatKind(N)),N)
plus(N,s(M)) -> U51(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
x(N,0()) -> U61(and(isNat(N),n__isNatKind(N)))
x(N,s(M)) -> U71(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
0() -> n__0()
plus(X1,X2) -> n__plus(X1,X2)
isNatKind(X) -> n__isNatKind(X)
s(X) -> n__s(X)
x(X1,X2) -> n__x(X1,X2)
and(X1,X2) -> n__and(X1,X2)
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__isNatKind(X)) -> isNatKind(X)
activate(n__s(X)) -> s(X)
activate(n__x(X1,X2)) -> x(X1,X2)
activate(n__and(X1,X2)) -> and(X1,X2)
activate(X) -> X

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 MYNAT complete Z

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 MYNAT complete Z

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
     , U12(tt(), V2) -> U13(isNat(activate(V2)))
     , U13(tt()) -> tt()
     , U21(tt(), V1) -> U22(isNat(activate(V1)))
     , U22(tt()) -> tt()
     , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
     , U32(tt(), V2) -> U33(isNat(activate(V2)))
     , U33(tt()) -> tt()
     , U41(tt(), N) -> activate(N)
     , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
     , U61(tt()) -> 0()
     , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
     , and(tt(), X) -> activate(X)
     , isNat(n__0()) -> tt()
     , isNat(n__plus(V1, V2)) ->
       U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
     , isNat(n__x(V1, V2)) ->
       U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatKind(n__0()) -> tt()
     , isNatKind(n__plus(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
     , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
     , isNatKind(n__x(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
     , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
     , plus(N, s(M)) ->
       U51(and(and(isNat(M), n__isNatKind(M)),
               n__and(isNat(N), n__isNatKind(N))),
           M,
           N)
     , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
     , x(N, s(M)) ->
       U71(and(and(isNat(M), n__isNatKind(M)),
               n__and(isNat(N), n__isNatKind(N))),
           M,
           N)
     , 0() -> n__0()
     , plus(X1, X2) -> n__plus(X1, X2)
     , isNatKind(X) -> n__isNatKind(X)
     , s(X) -> n__s(X)
     , x(X1, X2) -> n__x(X1, X2)
     , and(X1, X2) -> n__and(X1, X2)
     , activate(n__0()) -> 0()
     , activate(n__plus(X1, X2)) -> plus(X1, X2)
     , activate(n__isNatKind(X)) -> isNatKind(X)
     , activate(n__s(X)) -> s(X)
     , activate(n__x(X1, X2)) -> x(X1, X2)
     , activate(n__and(X1, X2)) -> and(X1, X2)
     , activate(X) -> X}

Proof Output:
  None of the processors succeeded.

  Details of failed attempt(s):
  -----------------------------
    1) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:

             {  1: U11^#(tt(), V1, V2) ->
                   c_0(U12^#(isNat(activate(V1)), activate(V2)))
              , 2: U12^#(tt(), V2) -> c_1(U13^#(isNat(activate(V2))))
              , 3: U13^#(tt()) -> c_2()
              , 4: U21^#(tt(), V1) -> c_3(U22^#(isNat(activate(V1))))
              , 5: U22^#(tt()) -> c_4()
              , 6: U31^#(tt(), V1, V2) ->
                   c_5(U32^#(isNat(activate(V1)), activate(V2)))
              , 7: U32^#(tt(), V2) -> c_6(U33^#(isNat(activate(V2))))
              , 8: U33^#(tt()) -> c_7()
              , 9: U41^#(tt(), N) -> c_8(activate^#(N))
              , 10: U51^#(tt(), M, N) -> c_9(s^#(plus(activate(N), activate(M))))
              , 11: U61^#(tt()) -> c_10(0^#())
              , 12: U71^#(tt(), M, N) ->
                    c_11(plus^#(x(activate(N), activate(M)), activate(N)))
              , 13: and^#(tt(), X) -> c_12(activate^#(X))
              , 14: isNat^#(n__0()) -> c_13()
              , 15: isNat^#(n__plus(V1, V2)) ->
                    c_14(U11^#(and(isNatKind(activate(V1)),
                                   n__isNatKind(activate(V2))),
                               activate(V1),
                               activate(V2)))
              , 16: isNat^#(n__s(V1)) ->
                    c_15(U21^#(isNatKind(activate(V1)), activate(V1)))
              , 17: isNat^#(n__x(V1, V2)) ->
                    c_16(U31^#(and(isNatKind(activate(V1)),
                                   n__isNatKind(activate(V2))),
                               activate(V1),
                               activate(V2)))
              , 18: isNatKind^#(n__0()) -> c_17()
              , 19: isNatKind^#(n__plus(V1, V2)) ->
                    c_18(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))))
              , 20: isNatKind^#(n__s(V1)) -> c_19(isNatKind^#(activate(V1)))
              , 21: isNatKind^#(n__x(V1, V2)) ->
                    c_20(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))))
              , 22: plus^#(N, 0()) ->
                    c_21(U41^#(and(isNat(N), n__isNatKind(N)), N))
              , 23: plus^#(N, s(M)) ->
                    c_22(U51^#(and(and(isNat(M), n__isNatKind(M)),
                                   n__and(isNat(N), n__isNatKind(N))),
                               M,
                               N))
              , 24: x^#(N, 0()) -> c_23(U61^#(and(isNat(N), n__isNatKind(N))))
              , 25: x^#(N, s(M)) ->
                    c_24(U71^#(and(and(isNat(M), n__isNatKind(M)),
                                   n__and(isNat(N), n__isNatKind(N))),
                               M,
                               N))
              , 26: 0^#() -> c_25()
              , 27: plus^#(X1, X2) -> c_26()
              , 28: isNatKind^#(X) -> c_27()
              , 29: s^#(X) -> c_28()
              , 30: x^#(X1, X2) -> c_29()
              , 31: and^#(X1, X2) -> c_30()
              , 32: activate^#(n__0()) -> c_31(0^#())
              , 33: activate^#(n__plus(X1, X2)) -> c_32(plus^#(X1, X2))
              , 34: activate^#(n__isNatKind(X)) -> c_33(isNatKind^#(X))
              , 35: activate^#(n__s(X)) -> c_34(s^#(X))
              , 36: activate^#(n__x(X1, X2)) -> c_35(x^#(X1, X2))
              , 37: activate^#(n__and(X1, X2)) -> c_36(and^#(X1, X2))
              , 38: activate^#(X) -> c_37()}

           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)

             ->{17}                                                      [     inherited      ]
                |
                `->{6}                                                   [     inherited      ]
                    |
                    `->{7}                                               [     inherited      ]
                        |
                        `->{8}                                           [         NA         ]

             ->{16}                                                      [     inherited      ]
                |
                `->{4}                                                   [     inherited      ]
                    |
                    `->{5}                                               [       MAYBE        ]

             ->{15}                                                      [     inherited      ]
                |
                `->{1}                                                   [     inherited      ]
                    |
                    `->{2}                                               [     inherited      ]
                        |
                        `->{3}                                           [         NA         ]

             ->{14}                                                      [    YES(?,O(1))     ]

             ->{9,22,33,13,37,21,34,20,19,12,25,36}                      [     inherited      ]
                |
                |->{18}                                                  [         NA         ]
                |
                |->{23}                                                  [     inherited      ]
                |   |
                |   `->{10}                                              [     inherited      ]
                |       |
                |       `->{29}                                          [         NA         ]
                |
                |->{24}                                                  [     inherited      ]
                |   |
                |   `->{11}                                              [     inherited      ]
                |       |
                |       `->{26}                                          [         NA         ]
                |
                |->{27}                                                  [         NA         ]
                |
                |->{28}                                                  [         NA         ]
                |
                |->{30}                                                  [         NA         ]
                |
                |->{31}                                                  [         NA         ]
                |
                |->{32}                                                  [     inherited      ]
                |   |
                |   `->{26}                                              [         NA         ]
                |
                |->{35}                                                  [     inherited      ]
                |   |
                |   `->{29}                                              [         NA         ]
                |
                `->{38}                                                  [         NA         ]



         Sub-problems:
         -------------
           * Path {9,22,33,13,37,21,34,20,19,12,25,36}: inherited
             ----------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{23}->{10}->{29}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{18}: NA
             ---------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{23}: inherited
             ----------------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{23}->{10}->{29}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{23}->{10}: inherited
             ----------------------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{23}->{10}->{29}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{23}->{10}->{29}: NA
             ---------------------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{24}: inherited
             ----------------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{24}->{11}->{26}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{24}->{11}: inherited
             ----------------------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{24}->{11}->{26}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{24}->{11}->{26}: NA
             ---------------------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{27}: NA
             ---------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{28}: NA
             ---------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{30}: NA
             ---------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{31}: NA
             ---------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{32}: inherited
             ----------------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{32}->{26}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{32}->{26}: NA
             ---------------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{35}: inherited
             ----------------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{35}->{29}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{35}->{29}: NA
             ---------------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{38}: NA
             ---------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {14}: YES(?,O(1))
             ----------------------

             The usable rules of this path are empty.

             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(U11) = {}, Uargs(U12) = {}, Uargs(isNat) = {},
                 Uargs(activate) = {}, Uargs(U13) = {}, Uargs(U21) = {},
                 Uargs(U22) = {}, Uargs(U31) = {}, Uargs(U32) = {}, Uargs(U33) = {},
                 Uargs(U41) = {}, Uargs(U51) = {}, Uargs(s) = {}, Uargs(plus) = {},
                 Uargs(U61) = {}, Uargs(U71) = {}, Uargs(x) = {}, Uargs(and) = {},
                 Uargs(n__plus) = {}, Uargs(isNatKind) = {},
                 Uargs(n__isNatKind) = {}, Uargs(n__s) = {}, Uargs(n__x) = {},
                 Uargs(n__and) = {}, Uargs(U11^#) = {}, Uargs(c_0) = {},
                 Uargs(U12^#) = {}, Uargs(c_1) = {}, Uargs(U13^#) = {},
                 Uargs(U21^#) = {}, Uargs(c_3) = {}, Uargs(U22^#) = {},
                 Uargs(U31^#) = {}, Uargs(c_5) = {}, Uargs(U32^#) = {},
                 Uargs(c_6) = {}, Uargs(U33^#) = {}, Uargs(U41^#) = {},
                 Uargs(c_8) = {}, Uargs(activate^#) = {}, Uargs(U51^#) = {},
                 Uargs(c_9) = {}, Uargs(s^#) = {}, Uargs(U61^#) = {},
                 Uargs(c_10) = {}, Uargs(U71^#) = {}, Uargs(c_11) = {},
                 Uargs(plus^#) = {}, Uargs(and^#) = {}, Uargs(c_12) = {},
                 Uargs(isNat^#) = {}, Uargs(c_14) = {}, Uargs(c_15) = {},
                 Uargs(c_16) = {}, Uargs(isNatKind^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}, Uargs(c_20) = {}, Uargs(c_21) = {},
                 Uargs(c_22) = {}, Uargs(x^#) = {}, Uargs(c_23) = {},
                 Uargs(c_24) = {}, Uargs(c_31) = {}, Uargs(c_32) = {},
                 Uargs(c_33) = {}, Uargs(c_34) = {}, Uargs(c_35) = {},
                 Uargs(c_36) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                U11(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                tt() = [0]
                U12(x1, x2) = [0] x1 + [0] x2 + [0]
                isNat(x1) = [0] x1 + [0]
                activate(x1) = [0] x1 + [0]
                U13(x1) = [0] x1 + [0]
                U21(x1, x2) = [0] x1 + [0] x2 + [0]
                U22(x1) = [0] x1 + [0]
                U31(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U32(x1, x2) = [0] x1 + [0] x2 + [0]
                U33(x1) = [0] x1 + [0]
                U41(x1, x2) = [0] x1 + [0] x2 + [0]
                U51(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                s(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                U61(x1) = [0] x1 + [0]
                0() = [0]
                U71(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                x(x1, x2) = [0] x1 + [0] x2 + [0]
                and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__0() = [0]
                n__plus(x1, x2) = [0] x1 + [0] x2 + [0]
                isNatKind(x1) = [0] x1 + [0]
                n__isNatKind(x1) = [0] x1 + [0]
                n__s(x1) = [0] x1 + [0]
                n__x(x1, x2) = [0] x1 + [0] x2 + [0]
                n__and(x1, x2) = [0] x1 + [0] x2 + [0]
                U11^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_0(x1) = [0] x1 + [0]
                U12^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_1(x1) = [0] x1 + [0]
                U13^#(x1) = [0] x1 + [0]
                c_2() = [0]
                U21^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_3(x1) = [0] x1 + [0]
                U22^#(x1) = [0] x1 + [0]
                c_4() = [0]
                U31^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_5(x1) = [0] x1 + [0]
                U32^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_6(x1) = [0] x1 + [0]
                U33^#(x1) = [0] x1 + [0]
                c_7() = [0]
                U41^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_8(x1) = [0] x1 + [0]
                activate^#(x1) = [0] x1 + [0]
                U51^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_9(x1) = [0] x1 + [0]
                s^#(x1) = [0] x1 + [0]
                U61^#(x1) = [0] x1 + [0]
                c_10(x1) = [0] x1 + [0]
                0^#() = [0]
                U71^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_11(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                and^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_12(x1) = [0] x1 + [0]
                isNat^#(x1) = [0] x1 + [0]
                c_13() = [0]
                c_14(x1) = [0] x1 + [0]
                c_15(x1) = [0] x1 + [0]
                c_16(x1) = [0] x1 + [0]
                isNatKind^#(x1) = [0] x1 + [0]
                c_17() = [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
                c_20(x1) = [0] x1 + [0]
                c_21(x1) = [0] x1 + [0]
                c_22(x1) = [0] x1 + [0]
                x^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_23(x1) = [0] x1 + [0]
                c_24(x1) = [0] x1 + [0]
                c_25() = [0]
                c_26() = [0]
                c_27() = [0]
                c_28() = [0]
                c_29() = [0]
                c_30() = [0]
                c_31(x1) = [0] x1 + [0]
                c_32(x1) = [0] x1 + [0]
                c_33(x1) = [0] x1 + [0]
                c_34(x1) = [0] x1 + [0]
                c_35(x1) = [0] x1 + [0]
                c_36(x1) = [0] x1 + [0]
                c_37() = [0]

             We apply the sub-processor on the resulting sub-problem:

             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    innermost DP runtime-complexity with respect to
               Strict Rules: {isNat^#(n__0()) -> c_13()}
               Weak Rules: {}

             Proof Output:
               The following argument positions are usable:
                 Uargs(isNat^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                n__0() = [7]
                isNat^#(x1) = [1] x1 + [7]
                c_13() = [1]

           * Path {15}: inherited
             --------------------

             This path is subsumed by the proof of path {15}->{1}->{2}->{3}.

           * Path {15}->{1}: inherited
             -------------------------

             This path is subsumed by the proof of path {15}->{1}->{2}->{3}.

           * Path {15}->{1}->{2}: inherited
             ------------------------------

             This path is subsumed by the proof of path {15}->{1}->{2}->{3}.

           * Path {15}->{1}->{2}->{3}: NA
             ----------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(X) -> n__isNatKind(X)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , x(X1, X2) -> n__x(X1, X2)
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {16}: inherited
             --------------------

             This path is subsumed by the proof of path {16}->{4}->{5}.

           * Path {16}->{4}: inherited
             -------------------------

             This path is subsumed by the proof of path {16}->{4}->{5}.

           * Path {16}->{4}->{5}: MAYBE
             --------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , and(tt(), X) -> activate(X)
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We apply the sub-processor on the resulting sub-problem:

             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    innermost runtime-complexity with respect to
               Rules:
                 {  U21^#(tt(), V1) -> c_3(U22^#(isNat(activate(V1))))
                  , isNat^#(n__s(V1)) ->
                    c_15(U21^#(isNatKind(activate(V1)), activate(V1)))
                  , U22^#(tt()) -> c_4()
                  , isNatKind(n__0()) -> tt()
                  , isNatKind(n__plus(V1, V2)) ->
                    and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                  , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                  , isNatKind(n__x(V1, V2)) ->
                    and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                  , isNatKind(X) -> n__isNatKind(X)
                  , activate(n__0()) -> 0()
                  , activate(n__plus(X1, X2)) -> plus(X1, X2)
                  , activate(n__isNatKind(X)) -> isNatKind(X)
                  , activate(n__s(X)) -> s(X)
                  , activate(n__x(X1, X2)) -> x(X1, X2)
                  , activate(n__and(X1, X2)) -> and(X1, X2)
                  , activate(X) -> X
                  , and(tt(), X) -> activate(X)
                  , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                  , plus(N, s(M)) ->
                    U51(and(and(isNat(M), n__isNatKind(M)),
                            n__and(isNat(N), n__isNatKind(N))),
                        M,
                        N)
                  , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                  , x(N, s(M)) ->
                    U71(and(and(isNat(M), n__isNatKind(M)),
                            n__and(isNat(N), n__isNatKind(N))),
                        M,
                        N)
                  , 0() -> n__0()
                  , plus(X1, X2) -> n__plus(X1, X2)
                  , s(X) -> n__s(X)
                  , x(X1, X2) -> n__x(X1, X2)
                  , and(X1, X2) -> n__and(X1, X2)
                  , U41(tt(), N) -> activate(N)
                  , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                  , U61(tt()) -> 0()
                  , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                  , isNat(n__0()) -> tt()
                  , isNat(n__plus(V1, V2)) ->
                    U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                        activate(V1),
                        activate(V2))
                  , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                  , isNat(n__x(V1, V2)) ->
                    U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                        activate(V1),
                        activate(V2))
                  , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                  , U21(tt(), V1) -> U22(isNat(activate(V1)))
                  , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                  , U12(tt(), V2) -> U13(isNat(activate(V2)))
                  , U22(tt()) -> tt()
                  , U32(tt(), V2) -> U33(isNat(activate(V2)))
                  , U13(tt()) -> tt()
                  , U33(tt()) -> tt()}

             Proof Output:
               The input cannot be shown compatible

           * Path {17}: inherited
             --------------------

             This path is subsumed by the proof of path {17}->{6}->{7}->{8}.

           * Path {17}->{6}: inherited
             -------------------------

             This path is subsumed by the proof of path {17}->{6}->{7}->{8}.

           * Path {17}->{6}->{7}: inherited
             ------------------------------

             This path is subsumed by the proof of path {17}->{6}->{7}->{8}.

           * Path {17}->{6}->{7}->{8}: NA
             ----------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(X) -> n__isNatKind(X)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , x(X1, X2) -> n__x(X1, X2)
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

    2) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible

    3) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.

    4) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 MYNAT complete Z

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 MYNAT complete Z

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    runtime-complexity with respect to
  Rules:
    {  U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
     , U12(tt(), V2) -> U13(isNat(activate(V2)))
     , U13(tt()) -> tt()
     , U21(tt(), V1) -> U22(isNat(activate(V1)))
     , U22(tt()) -> tt()
     , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
     , U32(tt(), V2) -> U33(isNat(activate(V2)))
     , U33(tt()) -> tt()
     , U41(tt(), N) -> activate(N)
     , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
     , U61(tt()) -> 0()
     , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
     , and(tt(), X) -> activate(X)
     , isNat(n__0()) -> tt()
     , isNat(n__plus(V1, V2)) ->
       U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
     , isNat(n__x(V1, V2)) ->
       U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatKind(n__0()) -> tt()
     , isNatKind(n__plus(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
     , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
     , isNatKind(n__x(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
     , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
     , plus(N, s(M)) ->
       U51(and(and(isNat(M), n__isNatKind(M)),
               n__and(isNat(N), n__isNatKind(N))),
           M,
           N)
     , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
     , x(N, s(M)) ->
       U71(and(and(isNat(M), n__isNatKind(M)),
               n__and(isNat(N), n__isNatKind(N))),
           M,
           N)
     , 0() -> n__0()
     , plus(X1, X2) -> n__plus(X1, X2)
     , isNatKind(X) -> n__isNatKind(X)
     , s(X) -> n__s(X)
     , x(X1, X2) -> n__x(X1, X2)
     , and(X1, X2) -> n__and(X1, X2)
     , activate(n__0()) -> 0()
     , activate(n__plus(X1, X2)) -> plus(X1, X2)
     , activate(n__isNatKind(X)) -> isNatKind(X)
     , activate(n__s(X)) -> s(X)
     , activate(n__x(X1, X2)) -> x(X1, X2)
     , activate(n__and(X1, X2)) -> and(X1, X2)
     , activate(X) -> X}

Proof Output:
  None of the processors succeeded.

  Details of failed attempt(s):
  -----------------------------
    1) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:

             {  1: U11^#(tt(), V1, V2) ->
                   c_0(U12^#(isNat(activate(V1)), activate(V2)))
              , 2: U12^#(tt(), V2) -> c_1(U13^#(isNat(activate(V2))))
              , 3: U13^#(tt()) -> c_2()
              , 4: U21^#(tt(), V1) -> c_3(U22^#(isNat(activate(V1))))
              , 5: U22^#(tt()) -> c_4()
              , 6: U31^#(tt(), V1, V2) ->
                   c_5(U32^#(isNat(activate(V1)), activate(V2)))
              , 7: U32^#(tt(), V2) -> c_6(U33^#(isNat(activate(V2))))
              , 8: U33^#(tt()) -> c_7()
              , 9: U41^#(tt(), N) -> c_8(activate^#(N))
              , 10: U51^#(tt(), M, N) -> c_9(s^#(plus(activate(N), activate(M))))
              , 11: U61^#(tt()) -> c_10(0^#())
              , 12: U71^#(tt(), M, N) ->
                    c_11(plus^#(x(activate(N), activate(M)), activate(N)))
              , 13: and^#(tt(), X) -> c_12(activate^#(X))
              , 14: isNat^#(n__0()) -> c_13()
              , 15: isNat^#(n__plus(V1, V2)) ->
                    c_14(U11^#(and(isNatKind(activate(V1)),
                                   n__isNatKind(activate(V2))),
                               activate(V1),
                               activate(V2)))
              , 16: isNat^#(n__s(V1)) ->
                    c_15(U21^#(isNatKind(activate(V1)), activate(V1)))
              , 17: isNat^#(n__x(V1, V2)) ->
                    c_16(U31^#(and(isNatKind(activate(V1)),
                                   n__isNatKind(activate(V2))),
                               activate(V1),
                               activate(V2)))
              , 18: isNatKind^#(n__0()) -> c_17()
              , 19: isNatKind^#(n__plus(V1, V2)) ->
                    c_18(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))))
              , 20: isNatKind^#(n__s(V1)) -> c_19(isNatKind^#(activate(V1)))
              , 21: isNatKind^#(n__x(V1, V2)) ->
                    c_20(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2))))
              , 22: plus^#(N, 0()) ->
                    c_21(U41^#(and(isNat(N), n__isNatKind(N)), N))
              , 23: plus^#(N, s(M)) ->
                    c_22(U51^#(and(and(isNat(M), n__isNatKind(M)),
                                   n__and(isNat(N), n__isNatKind(N))),
                               M,
                               N))
              , 24: x^#(N, 0()) -> c_23(U61^#(and(isNat(N), n__isNatKind(N))))
              , 25: x^#(N, s(M)) ->
                    c_24(U71^#(and(and(isNat(M), n__isNatKind(M)),
                                   n__and(isNat(N), n__isNatKind(N))),
                               M,
                               N))
              , 26: 0^#() -> c_25()
              , 27: plus^#(X1, X2) -> c_26(X1, X2)
              , 28: isNatKind^#(X) -> c_27(X)
              , 29: s^#(X) -> c_28(X)
              , 30: x^#(X1, X2) -> c_29(X1, X2)
              , 31: and^#(X1, X2) -> c_30(X1, X2)
              , 32: activate^#(n__0()) -> c_31(0^#())
              , 33: activate^#(n__plus(X1, X2)) -> c_32(plus^#(X1, X2))
              , 34: activate^#(n__isNatKind(X)) -> c_33(isNatKind^#(X))
              , 35: activate^#(n__s(X)) -> c_34(s^#(X))
              , 36: activate^#(n__x(X1, X2)) -> c_35(x^#(X1, X2))
              , 37: activate^#(n__and(X1, X2)) -> c_36(and^#(X1, X2))
              , 38: activate^#(X) -> c_37(X)}

           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)

             ->{17}                                                      [     inherited      ]
                |
                `->{6}                                                   [     inherited      ]
                    |
                    `->{7}                                               [     inherited      ]
                        |
                        `->{8}                                           [         NA         ]

             ->{16}                                                      [     inherited      ]
                |
                `->{4}                                                   [     inherited      ]
                    |
                    `->{5}                                               [       MAYBE        ]

             ->{15}                                                      [     inherited      ]
                |
                `->{1}                                                   [     inherited      ]
                    |
                    `->{2}                                               [     inherited      ]
                        |
                        `->{3}                                           [         NA         ]

             ->{14}                                                      [    YES(?,O(1))     ]

             ->{9,22,33,13,37,21,34,20,19,12,25,36}                      [     inherited      ]
                |
                |->{18}                                                  [         NA         ]
                |
                |->{23}                                                  [     inherited      ]
                |   |
                |   `->{10}                                              [     inherited      ]
                |       |
                |       `->{29}                                          [         NA         ]
                |
                |->{24}                                                  [     inherited      ]
                |   |
                |   `->{11}                                              [     inherited      ]
                |       |
                |       `->{26}                                          [         NA         ]
                |
                |->{27}                                                  [         NA         ]
                |
                |->{28}                                                  [         NA         ]
                |
                |->{30}                                                  [         NA         ]
                |
                |->{31}                                                  [         NA         ]
                |
                |->{32}                                                  [     inherited      ]
                |   |
                |   `->{26}                                              [         NA         ]
                |
                |->{35}                                                  [     inherited      ]
                |   |
                |   `->{29}                                              [         NA         ]
                |
                `->{38}                                                  [         NA         ]



         Sub-problems:
         -------------
           * Path {9,22,33,13,37,21,34,20,19,12,25,36}: inherited
             ----------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{23}->{10}->{29}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{18}: NA
             ---------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{23}: inherited
             ----------------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{23}->{10}->{29}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{23}->{10}: inherited
             ----------------------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{23}->{10}->{29}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{23}->{10}->{29}: NA
             ---------------------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{24}: inherited
             ----------------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{24}->{11}->{26}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{24}->{11}: inherited
             ----------------------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{24}->{11}->{26}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{24}->{11}->{26}: NA
             ---------------------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{27}: NA
             ---------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{28}: NA
             ---------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{30}: NA
             ---------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{31}: NA
             ---------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{32}: inherited
             ----------------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{32}->{26}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{32}->{26}: NA
             ---------------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{35}: inherited
             ----------------------------------------------------------

             This path is subsumed by the proof of path {9,22,33,13,37,21,34,20,19,12,25,36}->{35}->{29}.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{35}->{29}: NA
             ---------------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {9,22,33,13,37,21,34,20,19,12,25,36}->{38}: NA
             ---------------------------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , isNatKind(X) -> n__isNatKind(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {14}: YES(?,O(1))
             ----------------------

             The usable rules of this path are empty.

             The weightgap principle applies, using the following adequate RMI:
               The following argument positions are usable:
                 Uargs(U11) = {}, Uargs(U12) = {}, Uargs(isNat) = {},
                 Uargs(activate) = {}, Uargs(U13) = {}, Uargs(U21) = {},
                 Uargs(U22) = {}, Uargs(U31) = {}, Uargs(U32) = {}, Uargs(U33) = {},
                 Uargs(U41) = {}, Uargs(U51) = {}, Uargs(s) = {}, Uargs(plus) = {},
                 Uargs(U61) = {}, Uargs(U71) = {}, Uargs(x) = {}, Uargs(and) = {},
                 Uargs(n__plus) = {}, Uargs(isNatKind) = {},
                 Uargs(n__isNatKind) = {}, Uargs(n__s) = {}, Uargs(n__x) = {},
                 Uargs(n__and) = {}, Uargs(U11^#) = {}, Uargs(c_0) = {},
                 Uargs(U12^#) = {}, Uargs(c_1) = {}, Uargs(U13^#) = {},
                 Uargs(U21^#) = {}, Uargs(c_3) = {}, Uargs(U22^#) = {},
                 Uargs(U31^#) = {}, Uargs(c_5) = {}, Uargs(U32^#) = {},
                 Uargs(c_6) = {}, Uargs(U33^#) = {}, Uargs(U41^#) = {},
                 Uargs(c_8) = {}, Uargs(activate^#) = {}, Uargs(U51^#) = {},
                 Uargs(c_9) = {}, Uargs(s^#) = {}, Uargs(U61^#) = {},
                 Uargs(c_10) = {}, Uargs(U71^#) = {}, Uargs(c_11) = {},
                 Uargs(plus^#) = {}, Uargs(and^#) = {}, Uargs(c_12) = {},
                 Uargs(isNat^#) = {}, Uargs(c_14) = {}, Uargs(c_15) = {},
                 Uargs(c_16) = {}, Uargs(isNatKind^#) = {}, Uargs(c_18) = {},
                 Uargs(c_19) = {}, Uargs(c_20) = {}, Uargs(c_21) = {},
                 Uargs(c_22) = {}, Uargs(x^#) = {}, Uargs(c_23) = {},
                 Uargs(c_24) = {}, Uargs(c_26) = {}, Uargs(c_27) = {},
                 Uargs(c_28) = {}, Uargs(c_29) = {}, Uargs(c_30) = {},
                 Uargs(c_31) = {}, Uargs(c_32) = {}, Uargs(c_33) = {},
                 Uargs(c_34) = {}, Uargs(c_35) = {}, Uargs(c_36) = {},
                 Uargs(c_37) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                U11(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                tt() = [0]
                U12(x1, x2) = [0] x1 + [0] x2 + [0]
                isNat(x1) = [0] x1 + [0]
                activate(x1) = [0] x1 + [0]
                U13(x1) = [0] x1 + [0]
                U21(x1, x2) = [0] x1 + [0] x2 + [0]
                U22(x1) = [0] x1 + [0]
                U31(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U32(x1, x2) = [0] x1 + [0] x2 + [0]
                U33(x1) = [0] x1 + [0]
                U41(x1, x2) = [0] x1 + [0] x2 + [0]
                U51(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                s(x1) = [0] x1 + [0]
                plus(x1, x2) = [0] x1 + [0] x2 + [0]
                U61(x1) = [0] x1 + [0]
                0() = [0]
                U71(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                x(x1, x2) = [0] x1 + [0] x2 + [0]
                and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__0() = [0]
                n__plus(x1, x2) = [0] x1 + [0] x2 + [0]
                isNatKind(x1) = [0] x1 + [0]
                n__isNatKind(x1) = [0] x1 + [0]
                n__s(x1) = [0] x1 + [0]
                n__x(x1, x2) = [0] x1 + [0] x2 + [0]
                n__and(x1, x2) = [0] x1 + [0] x2 + [0]
                U11^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_0(x1) = [0] x1 + [0]
                U12^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_1(x1) = [0] x1 + [0]
                U13^#(x1) = [0] x1 + [0]
                c_2() = [0]
                U21^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_3(x1) = [0] x1 + [0]
                U22^#(x1) = [0] x1 + [0]
                c_4() = [0]
                U31^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_5(x1) = [0] x1 + [0]
                U32^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_6(x1) = [0] x1 + [0]
                U33^#(x1) = [0] x1 + [0]
                c_7() = [0]
                U41^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_8(x1) = [0] x1 + [0]
                activate^#(x1) = [0] x1 + [0]
                U51^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_9(x1) = [0] x1 + [0]
                s^#(x1) = [0] x1 + [0]
                U61^#(x1) = [0] x1 + [0]
                c_10(x1) = [0] x1 + [0]
                0^#() = [0]
                U71^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_11(x1) = [0] x1 + [0]
                plus^#(x1, x2) = [0] x1 + [0] x2 + [0]
                and^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_12(x1) = [0] x1 + [0]
                isNat^#(x1) = [0] x1 + [0]
                c_13() = [0]
                c_14(x1) = [0] x1 + [0]
                c_15(x1) = [0] x1 + [0]
                c_16(x1) = [0] x1 + [0]
                isNatKind^#(x1) = [0] x1 + [0]
                c_17() = [0]
                c_18(x1) = [0] x1 + [0]
                c_19(x1) = [0] x1 + [0]
                c_20(x1) = [0] x1 + [0]
                c_21(x1) = [0] x1 + [0]
                c_22(x1) = [0] x1 + [0]
                x^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_23(x1) = [0] x1 + [0]
                c_24(x1) = [0] x1 + [0]
                c_25() = [0]
                c_26(x1, x2) = [0] x1 + [0] x2 + [0]
                c_27(x1) = [0] x1 + [0]
                c_28(x1) = [0] x1 + [0]
                c_29(x1, x2) = [0] x1 + [0] x2 + [0]
                c_30(x1, x2) = [0] x1 + [0] x2 + [0]
                c_31(x1) = [0] x1 + [0]
                c_32(x1) = [0] x1 + [0]
                c_33(x1) = [0] x1 + [0]
                c_34(x1) = [0] x1 + [0]
                c_35(x1) = [0] x1 + [0]
                c_36(x1) = [0] x1 + [0]
                c_37(x1) = [0] x1 + [0]

             We apply the sub-processor on the resulting sub-problem:

             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           YES(?,O(1))
             Input Problem:    DP runtime-complexity with respect to
               Strict Rules: {isNat^#(n__0()) -> c_13()}
               Weak Rules: {}

             Proof Output:
               The following argument positions are usable:
                 Uargs(isNat^#) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                n__0() = [7]
                isNat^#(x1) = [1] x1 + [7]
                c_13() = [1]

           * Path {15}: inherited
             --------------------

             This path is subsumed by the proof of path {15}->{1}->{2}->{3}.

           * Path {15}->{1}: inherited
             -------------------------

             This path is subsumed by the proof of path {15}->{1}->{2}->{3}.

           * Path {15}->{1}->{2}: inherited
             ------------------------------

             This path is subsumed by the proof of path {15}->{1}->{2}->{3}.

           * Path {15}->{1}->{2}->{3}: NA
             ----------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(X) -> n__isNatKind(X)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , x(X1, X2) -> n__x(X1, X2)
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {16}: inherited
             --------------------

             This path is subsumed by the proof of path {16}->{4}->{5}.

           * Path {16}->{4}: inherited
             -------------------------

             This path is subsumed by the proof of path {16}->{4}->{5}.

           * Path {16}->{4}->{5}: MAYBE
             --------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , and(tt(), X) -> activate(X)
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , x(X1, X2) -> n__x(X1, X2)
                , and(X1, X2) -> n__and(X1, X2)
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We apply the sub-processor on the resulting sub-problem:

             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    runtime-complexity with respect to
               Rules:
                 {  U21^#(tt(), V1) -> c_3(U22^#(isNat(activate(V1))))
                  , isNat^#(n__s(V1)) ->
                    c_15(U21^#(isNatKind(activate(V1)), activate(V1)))
                  , U22^#(tt()) -> c_4()
                  , isNatKind(n__0()) -> tt()
                  , isNatKind(n__plus(V1, V2)) ->
                    and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                  , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                  , isNatKind(n__x(V1, V2)) ->
                    and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                  , isNatKind(X) -> n__isNatKind(X)
                  , activate(n__0()) -> 0()
                  , activate(n__plus(X1, X2)) -> plus(X1, X2)
                  , activate(n__isNatKind(X)) -> isNatKind(X)
                  , activate(n__s(X)) -> s(X)
                  , activate(n__x(X1, X2)) -> x(X1, X2)
                  , activate(n__and(X1, X2)) -> and(X1, X2)
                  , activate(X) -> X
                  , and(tt(), X) -> activate(X)
                  , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                  , plus(N, s(M)) ->
                    U51(and(and(isNat(M), n__isNatKind(M)),
                            n__and(isNat(N), n__isNatKind(N))),
                        M,
                        N)
                  , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                  , x(N, s(M)) ->
                    U71(and(and(isNat(M), n__isNatKind(M)),
                            n__and(isNat(N), n__isNatKind(N))),
                        M,
                        N)
                  , 0() -> n__0()
                  , plus(X1, X2) -> n__plus(X1, X2)
                  , s(X) -> n__s(X)
                  , x(X1, X2) -> n__x(X1, X2)
                  , and(X1, X2) -> n__and(X1, X2)
                  , U41(tt(), N) -> activate(N)
                  , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                  , U61(tt()) -> 0()
                  , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                  , isNat(n__0()) -> tt()
                  , isNat(n__plus(V1, V2)) ->
                    U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                        activate(V1),
                        activate(V2))
                  , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                  , isNat(n__x(V1, V2)) ->
                    U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                        activate(V1),
                        activate(V2))
                  , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                  , U21(tt(), V1) -> U22(isNat(activate(V1)))
                  , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                  , U12(tt(), V2) -> U13(isNat(activate(V2)))
                  , U22(tt()) -> tt()
                  , U32(tt(), V2) -> U33(isNat(activate(V2)))
                  , U13(tt()) -> tt()
                  , U33(tt()) -> tt()}

             Proof Output:
               The input cannot be shown compatible

           * Path {17}: inherited
             --------------------

             This path is subsumed by the proof of path {17}->{6}->{7}->{8}.

           * Path {17}->{6}: inherited
             -------------------------

             This path is subsumed by the proof of path {17}->{6}->{7}->{8}.

           * Path {17}->{6}->{7}: inherited
             ------------------------------

             This path is subsumed by the proof of path {17}->{6}->{7}->{8}.

           * Path {17}->{6}->{7}->{8}: NA
             ----------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__plus(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(n__x(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
                , isNatKind(X) -> n__isNatKind(X)
                , and(X1, X2) -> n__and(X1, X2)
                , activate(n__0()) -> 0()
                , activate(n__plus(X1, X2)) -> plus(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__x(X1, X2)) -> x(X1, X2)
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(X) -> X
                , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N)
                , plus(N, s(M)) ->
                  U51(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N)))
                , x(N, s(M)) ->
                  U71(and(and(isNat(M), n__isNatKind(M)),
                          n__and(isNat(N), n__isNatKind(N))),
                      M,
                      N)
                , 0() -> n__0()
                , plus(X1, X2) -> n__plus(X1, X2)
                , s(X) -> n__s(X)
                , x(X1, X2) -> n__x(X1, X2)
                , U41(tt(), N) -> activate(N)
                , U51(tt(), M, N) -> s(plus(activate(N), activate(M)))
                , U61(tt()) -> 0()
                , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
                , isNat(n__0()) -> tt()
                , isNat(n__plus(V1, V2)) ->
                  U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNat(n__x(V1, V2)) ->
                  U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2))
                , U12(tt(), V2) -> U13(isNat(activate(V2)))
                , U22(tt()) -> tt()
                , U32(tt(), V2) -> U33(isNat(activate(V2)))
                , U13(tt()) -> tt()
                , U33(tt()) -> tt()}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

    2) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible

    3) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.

    4) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.