Problem Transformed CSR 04 LengthOfFiniteLists complete Z

Tool CaT

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

stdout:

MAYBE

Problem:
zeros() -> cons(0(),n__zeros())
U11(tt(),V1) -> U12(isNatList(activate(V1)))
U12(tt()) -> tt()
U21(tt(),V1) -> U22(isNat(activate(V1)))
U22(tt()) -> tt()
U31(tt(),V) -> U32(isNatList(activate(V)))
U32(tt()) -> tt()
U41(tt(),V1,V2) -> U42(isNat(activate(V1)),activate(V2))
U42(tt(),V2) -> U43(isNatIList(activate(V2)))
U43(tt()) -> tt()
U51(tt(),V1,V2) -> U52(isNat(activate(V1)),activate(V2))
U52(tt(),V2) -> U53(isNatList(activate(V2)))
U53(tt()) -> tt()
U61(tt(),L) -> s(length(activate(L)))
and(tt(),X) -> activate(X)
isNat(n__0()) -> tt()
isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)),activate(V1))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatIList(V) -> U31(isNatIListKind(activate(V)),activate(V))
isNatIList(n__zeros()) -> tt()
isNatIList(n__cons(V1,V2)) ->
U41(and(isNatKind(activate(V1)),n__isNatIListKind(activate(V2))),activate(V1),activate(V2))
isNatIListKind(n__nil()) -> tt()
isNatIListKind(n__zeros()) -> tt()
isNatIListKind(n__cons(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatIListKind(activate(V2)))
isNatKind(n__0()) -> tt()
isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
isNatKind(n__s(V1)) -> isNatKind(activate(V1))
isNatList(n__nil()) -> tt()
isNatList(n__cons(V1,V2)) ->
U51(and(isNatKind(activate(V1)),n__isNatIListKind(activate(V2))),activate(V1),activate(V2))
length(nil()) -> 0()
length(cons(N,L)) ->
U61(and(and(isNatList(activate(L)),n__isNatIListKind(activate(L))),n__and
                                                                    (
                                                                    isNat(N),n__isNatKind(N))),
     activate(L))
zeros() -> n__zeros()
0() -> n__0()
length(X) -> n__length(X)
s(X) -> n__s(X)
cons(X1,X2) -> n__cons(X1,X2)
isNatIListKind(X) -> n__isNatIListKind(X)
nil() -> n__nil()
and(X1,X2) -> n__and(X1,X2)
isNatKind(X) -> n__isNatKind(X)
activate(n__zeros()) -> zeros()
activate(n__0()) -> 0()
activate(n__length(X)) -> length(X)
activate(n__s(X)) -> s(X)
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__isNatIListKind(X)) -> isNatIListKind(X)
activate(n__nil()) -> nil()
activate(n__and(X1,X2)) -> and(X1,X2)
activate(n__isNatKind(X)) -> isNatKind(X)
activate(X) -> X

Proof:
Open

Tool IRC1

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

stdout:

MAYBE

Tool IRC2

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

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  zeros() -> cons(0(), n__zeros())
     , U11(tt(), V1) -> U12(isNatList(activate(V1)))
     , U12(tt()) -> tt()
     , U21(tt(), V1) -> U22(isNat(activate(V1)))
     , U22(tt()) -> tt()
     , U31(tt(), V) -> U32(isNatList(activate(V)))
     , U32(tt()) -> tt()
     , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2))
     , U42(tt(), V2) -> U43(isNatIList(activate(V2)))
     , U43(tt()) -> tt()
     , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
     , U52(tt(), V2) -> U53(isNatList(activate(V2)))
     , U53(tt()) -> tt()
     , U61(tt(), L) -> s(length(activate(L)))
     , and(tt(), X) -> activate(X)
     , isNat(n__0()) -> tt()
     , isNat(n__length(V1)) ->
       U11(isNatIListKind(activate(V1)), activate(V1))
     , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
     , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V))
     , isNatIList(n__zeros()) -> tt()
     , isNatIList(n__cons(V1, V2)) ->
       U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatIListKind(n__nil()) -> tt()
     , isNatIListKind(n__zeros()) -> tt()
     , isNatIListKind(n__cons(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
     , isNatKind(n__0()) -> tt()
     , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
     , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
     , isNatList(n__nil()) -> tt()
     , isNatList(n__cons(V1, V2)) ->
       U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , length(nil()) -> 0()
     , length(cons(N, L)) ->
       U61(and(and(isNatList(activate(L)),
                   n__isNatIListKind(activate(L))),
               n__and(isNat(N), n__isNatKind(N))),
           activate(L))
     , zeros() -> n__zeros()
     , 0() -> n__0()
     , length(X) -> n__length(X)
     , s(X) -> n__s(X)
     , cons(X1, X2) -> n__cons(X1, X2)
     , isNatIListKind(X) -> n__isNatIListKind(X)
     , nil() -> n__nil()
     , and(X1, X2) -> n__and(X1, X2)
     , isNatKind(X) -> n__isNatKind(X)
     , activate(n__zeros()) -> zeros()
     , activate(n__0()) -> 0()
     , activate(n__length(X)) -> length(X)
     , activate(n__s(X)) -> s(X)
     , activate(n__cons(X1, X2)) -> cons(X1, X2)
     , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
     , activate(n__nil()) -> nil()
     , activate(n__and(X1, X2)) -> and(X1, X2)
     , activate(n__isNatKind(X)) -> isNatKind(X)
     , 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: zeros^#() -> c_0(cons^#(0(), n__zeros()))
              , 2: U11^#(tt(), V1) -> c_1(U12^#(isNatList(activate(V1))))
              , 3: U12^#(tt()) -> c_2()
              , 4: U21^#(tt(), V1) -> c_3(U22^#(isNat(activate(V1))))
              , 5: U22^#(tt()) -> c_4()
              , 6: U31^#(tt(), V) -> c_5(U32^#(isNatList(activate(V))))
              , 7: U32^#(tt()) -> c_6()
              , 8: U41^#(tt(), V1, V2) ->
                   c_7(U42^#(isNat(activate(V1)), activate(V2)))
              , 9: U42^#(tt(), V2) -> c_8(U43^#(isNatIList(activate(V2))))
              , 10: U43^#(tt()) -> c_9()
              , 11: U51^#(tt(), V1, V2) ->
                    c_10(U52^#(isNat(activate(V1)), activate(V2)))
              , 12: U52^#(tt(), V2) -> c_11(U53^#(isNatList(activate(V2))))
              , 13: U53^#(tt()) -> c_12()
              , 14: U61^#(tt(), L) -> c_13(s^#(length(activate(L))))
              , 15: and^#(tt(), X) -> c_14(activate^#(X))
              , 16: isNat^#(n__0()) -> c_15()
              , 17: isNat^#(n__length(V1)) ->
                    c_16(U11^#(isNatIListKind(activate(V1)), activate(V1)))
              , 18: isNat^#(n__s(V1)) ->
                    c_17(U21^#(isNatKind(activate(V1)), activate(V1)))
              , 19: isNatIList^#(V) ->
                    c_18(U31^#(isNatIListKind(activate(V)), activate(V)))
              , 20: isNatIList^#(n__zeros()) -> c_19()
              , 21: isNatIList^#(n__cons(V1, V2)) ->
                    c_20(U41^#(and(isNatKind(activate(V1)),
                                   n__isNatIListKind(activate(V2))),
                               activate(V1),
                               activate(V2)))
              , 22: isNatIListKind^#(n__nil()) -> c_21()
              , 23: isNatIListKind^#(n__zeros()) -> c_22()
              , 24: isNatIListKind^#(n__cons(V1, V2)) ->
                    c_23(and^#(isNatKind(activate(V1)),
                               n__isNatIListKind(activate(V2))))
              , 25: isNatKind^#(n__0()) -> c_24()
              , 26: isNatKind^#(n__length(V1)) ->
                    c_25(isNatIListKind^#(activate(V1)))
              , 27: isNatKind^#(n__s(V1)) -> c_26(isNatKind^#(activate(V1)))
              , 28: isNatList^#(n__nil()) -> c_27()
              , 29: isNatList^#(n__cons(V1, V2)) ->
                    c_28(U51^#(and(isNatKind(activate(V1)),
                                   n__isNatIListKind(activate(V2))),
                               activate(V1),
                               activate(V2)))
              , 30: length^#(nil()) -> c_29(0^#())
              , 31: length^#(cons(N, L)) ->
                    c_30(U61^#(and(and(isNatList(activate(L)),
                                       n__isNatIListKind(activate(L))),
                                   n__and(isNat(N), n__isNatKind(N))),
                               activate(L)))
              , 32: zeros^#() -> c_31()
              , 33: 0^#() -> c_32()
              , 34: length^#(X) -> c_33()
              , 35: s^#(X) -> c_34()
              , 36: cons^#(X1, X2) -> c_35()
              , 37: isNatIListKind^#(X) -> c_36()
              , 38: nil^#() -> c_37()
              , 39: and^#(X1, X2) -> c_38()
              , 40: isNatKind^#(X) -> c_39()
              , 41: activate^#(n__zeros()) -> c_40(zeros^#())
              , 42: activate^#(n__0()) -> c_41(0^#())
              , 43: activate^#(n__length(X)) -> c_42(length^#(X))
              , 44: activate^#(n__s(X)) -> c_43(s^#(X))
              , 45: activate^#(n__cons(X1, X2)) -> c_44(cons^#(X1, X2))
              , 46: activate^#(n__isNatIListKind(X)) -> c_45(isNatIListKind^#(X))
              , 47: activate^#(n__nil()) -> c_46(nil^#())
              , 48: activate^#(n__and(X1, X2)) -> c_47(and^#(X1, X2))
              , 49: activate^#(n__isNatKind(X)) -> c_48(isNatKind^#(X))
              , 50: activate^#(X) -> c_49()}

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

             ->{29}                                                      [     inherited      ]
                |
                `->{11}                                                  [     inherited      ]
                    |
                    `->{12}                                              [     inherited      ]
                        |
                        `->{13}                                          [         NA         ]

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

             ->{21}                                                      [     inherited      ]
                |
                `->{8}                                                   [     inherited      ]
                    |
                    `->{9}                                               [     inherited      ]
                        |
                        `->{10}                                          [         NA         ]

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

             ->{19}                                                      [     inherited      ]
                |
                `->{6}                                                   [     inherited      ]
                    |
                    `->{7}                                               [       MAYBE        ]

             ->{18}                                                      [     inherited      ]
                |
                `->{4}                                                   [     inherited      ]
                    |
                    `->{5}                                               [         NA         ]

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

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

             ->{15,48,24,46,26,49,27}                                    [     inherited      ]
                |
                |->{22}                                                  [         NA         ]
                |
                |->{23}                                                  [         NA         ]
                |
                |->{25}                                                  [         NA         ]
                |
                |->{37}                                                  [         NA         ]
                |
                |->{39}                                                  [         NA         ]
                |
                |->{40}                                                  [         NA         ]
                |
                |->{41}                                                  [     inherited      ]
                |   |
                |   |->{1}                                               [     inherited      ]
                |   |   |
                |   |   `->{36}                                          [         NA         ]
                |   |
                |   `->{32}                                              [         NA         ]
                |
                |->{42}                                                  [     inherited      ]
                |   |
                |   `->{33}                                              [         NA         ]
                |
                |->{43}                                                  [     inherited      ]
                |   |
                |   |->{30}                                              [     inherited      ]
                |   |   |
                |   |   `->{33}                                          [         NA         ]
                |   |
                |   |->{31}                                              [     inherited      ]
                |   |   |
                |   |   `->{14}                                          [     inherited      ]
                |   |       |
                |   |       `->{35}                                      [         NA         ]
                |   |
                |   `->{34}                                              [         NA         ]
                |
                |->{44}                                                  [     inherited      ]
                |   |
                |   `->{35}                                              [         NA         ]
                |
                |->{45}                                                  [     inherited      ]
                |   |
                |   `->{36}                                              [         NA         ]
                |
                |->{47}                                                  [     inherited      ]
                |   |
                |   `->{38}                                              [         NA         ]
                |
                `->{50}                                                  [         NA         ]



         Sub-problems:
         -------------
           * Path {15,48,24,46,26,49,27}: inherited
             --------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{47}->{38}.

           * Path {15,48,24,46,26,49,27}->{22}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{23}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{25}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{37}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{39}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{40}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{41}: inherited
             --------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{41}->{1}->{36}.

           * Path {15,48,24,46,26,49,27}->{41}->{1}: inherited
             -------------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{41}->{1}->{36}.

           * Path {15,48,24,46,26,49,27}->{41}->{1}->{36}: NA
             ------------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{41}->{32}: NA
             -------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{42}: inherited
             --------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{42}->{33}.

           * Path {15,48,24,46,26,49,27}->{42}->{33}: NA
             -------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{43}: inherited
             --------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{43}->{31}->{14}->{35}.

           * Path {15,48,24,46,26,49,27}->{43}->{30}: inherited
             --------------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{43}->{30}->{33}.

           * Path {15,48,24,46,26,49,27}->{43}->{30}->{33}: NA
             -------------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{43}->{31}: inherited
             --------------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{43}->{31}->{14}->{35}.

           * Path {15,48,24,46,26,49,27}->{43}->{31}->{14}: inherited
             --------------------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{43}->{31}->{14}->{35}.

           * Path {15,48,24,46,26,49,27}->{43}->{31}->{14}->{35}: NA
             -------------------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{43}->{34}: NA
             -------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{44}: inherited
             --------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{44}->{35}.

           * Path {15,48,24,46,26,49,27}->{44}->{35}: NA
             -------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{45}: inherited
             --------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{45}->{36}.

           * Path {15,48,24,46,26,49,27}->{45}->{36}: NA
             -------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{47}: inherited
             --------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{47}->{38}.

           * Path {15,48,24,46,26,49,27}->{47}->{38}: NA
             -------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{50}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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}: 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(cons) = {}, Uargs(U11) = {}, Uargs(U12) = {},
                 Uargs(isNatList) = {}, Uargs(activate) = {}, Uargs(U21) = {},
                 Uargs(U22) = {}, Uargs(isNat) = {}, Uargs(U31) = {},
                 Uargs(U32) = {}, Uargs(U41) = {}, Uargs(U42) = {}, Uargs(U43) = {},
                 Uargs(isNatIList) = {}, Uargs(U51) = {}, Uargs(U52) = {},
                 Uargs(U53) = {}, Uargs(U61) = {}, Uargs(s) = {},
                 Uargs(length) = {}, Uargs(and) = {}, Uargs(n__length) = {},
                 Uargs(isNatIListKind) = {}, Uargs(n__s) = {},
                 Uargs(isNatKind) = {}, Uargs(n__cons) = {},
                 Uargs(n__isNatIListKind) = {}, Uargs(n__and) = {},
                 Uargs(n__isNatKind) = {}, Uargs(c_0) = {}, Uargs(cons^#) = {},
                 Uargs(U11^#) = {}, Uargs(c_1) = {}, Uargs(U12^#) = {},
                 Uargs(U21^#) = {}, Uargs(c_3) = {}, Uargs(U22^#) = {},
                 Uargs(U31^#) = {}, Uargs(c_5) = {}, Uargs(U32^#) = {},
                 Uargs(U41^#) = {}, Uargs(c_7) = {}, Uargs(U42^#) = {},
                 Uargs(c_8) = {}, Uargs(U43^#) = {}, Uargs(U51^#) = {},
                 Uargs(c_10) = {}, Uargs(U52^#) = {}, Uargs(c_11) = {},
                 Uargs(U53^#) = {}, Uargs(U61^#) = {}, Uargs(c_13) = {},
                 Uargs(s^#) = {}, Uargs(and^#) = {}, Uargs(c_14) = {},
                 Uargs(activate^#) = {}, Uargs(isNat^#) = {}, Uargs(c_16) = {},
                 Uargs(c_17) = {}, Uargs(isNatIList^#) = {}, Uargs(c_18) = {},
                 Uargs(c_20) = {}, Uargs(isNatIListKind^#) = {}, Uargs(c_23) = {},
                 Uargs(isNatKind^#) = {}, Uargs(c_25) = {}, Uargs(c_26) = {},
                 Uargs(isNatList^#) = {}, Uargs(c_28) = {}, Uargs(length^#) = {},
                 Uargs(c_29) = {}, Uargs(c_30) = {}, Uargs(c_40) = {},
                 Uargs(c_41) = {}, Uargs(c_42) = {}, Uargs(c_43) = {},
                 Uargs(c_44) = {}, Uargs(c_45) = {}, Uargs(c_46) = {},
                 Uargs(c_47) = {}, Uargs(c_48) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                zeros() = [0]
                cons(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                n__zeros() = [0]
                U11(x1, x2) = [0] x1 + [0] x2 + [0]
                tt() = [0]
                U12(x1) = [0] x1 + [0]
                isNatList(x1) = [0] x1 + [0]
                activate(x1) = [0] x1 + [0]
                U21(x1, x2) = [0] x1 + [0] x2 + [0]
                U22(x1) = [0] x1 + [0]
                isNat(x1) = [0] x1 + [0]
                U31(x1, x2) = [0] x1 + [0] x2 + [0]
                U32(x1) = [0] x1 + [0]
                U41(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U42(x1, x2) = [0] x1 + [0] x2 + [0]
                U43(x1) = [0] x1 + [0]
                isNatIList(x1) = [0] x1 + [0]
                U51(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U52(x1, x2) = [0] x1 + [0] x2 + [0]
                U53(x1) = [0] x1 + [0]
                U61(x1, x2) = [0] x1 + [0] x2 + [0]
                s(x1) = [0] x1 + [0]
                length(x1) = [0] x1 + [0]
                and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__0() = [0]
                n__length(x1) = [0] x1 + [0]
                isNatIListKind(x1) = [0] x1 + [0]
                n__s(x1) = [0] x1 + [0]
                isNatKind(x1) = [0] x1 + [0]
                n__cons(x1, x2) = [0] x1 + [0] x2 + [0]
                n__isNatIListKind(x1) = [0] x1 + [0]
                n__nil() = [0]
                nil() = [0]
                n__and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__isNatKind(x1) = [0] x1 + [0]
                zeros^#() = [0]
                c_0(x1) = [0] x1 + [0]
                cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
                U11^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_1(x1) = [0] x1 + [0]
                U12^#(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) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                U32^#(x1) = [0] x1 + [0]
                c_6() = [0]
                U41^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_7(x1) = [0] x1 + [0]
                U42^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_8(x1) = [0] x1 + [0]
                U43^#(x1) = [0] x1 + [0]
                c_9() = [0]
                U51^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                U52^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_11(x1) = [0] x1 + [0]
                U53^#(x1) = [0] x1 + [0]
                c_12() = [0]
                U61^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13(x1) = [0] x1 + [0]
                s^#(x1) = [0] x1 + [0]
                and^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_14(x1) = [0] x1 + [0]
                activate^#(x1) = [0] x1 + [0]
                isNat^#(x1) = [0] x1 + [0]
                c_15() = [0]
                c_16(x1) = [0] x1 + [0]
                c_17(x1) = [0] x1 + [0]
                isNatIList^#(x1) = [0] x1 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19() = [0]
                c_20(x1) = [0] x1 + [0]
                isNatIListKind^#(x1) = [0] x1 + [0]
                c_21() = [0]
                c_22() = [0]
                c_23(x1) = [0] x1 + [0]
                isNatKind^#(x1) = [0] x1 + [0]
                c_24() = [0]
                c_25(x1) = [0] x1 + [0]
                c_26(x1) = [0] x1 + [0]
                isNatList^#(x1) = [0] x1 + [0]
                c_27() = [0]
                c_28(x1) = [0] x1 + [0]
                length^#(x1) = [0] x1 + [0]
                c_29(x1) = [0] x1 + [0]
                0^#() = [0]
                c_30(x1) = [0] x1 + [0]
                c_31() = [0]
                c_32() = [0]
                c_33() = [0]
                c_34() = [0]
                c_35() = [0]
                c_36() = [0]
                nil^#() = [0]
                c_37() = [0]
                c_38() = [0]
                c_39() = [0]
                c_40(x1) = [0] x1 + [0]
                c_41(x1) = [0] x1 + [0]
                c_42(x1) = [0] x1 + [0]
                c_43(x1) = [0] x1 + [0]
                c_44(x1) = [0] x1 + [0]
                c_45(x1) = [0] x1 + [0]
                c_46(x1) = [0] x1 + [0]
                c_47(x1) = [0] x1 + [0]
                c_48(x1) = [0] x1 + [0]
                c_49() = [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_15()}
               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_15() = [1]

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

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

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

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

           * Path {17}->{2}->{3}: NA
             -----------------------

             The usable rules for this path are:

               {  isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , isNatKind(X) -> n__isNatKind(X)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {18}: inherited
             --------------------

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

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

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

           * Path {18}->{4}->{5}: NA
             -----------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {19}: inherited
             --------------------

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

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

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

           * Path {19}->{6}->{7}: MAYBE
             --------------------------

             The usable rules for this path are:

               {  isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , isNatKind(X) -> n__isNatKind(X)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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:
                 {  U31^#(tt(), V) -> c_5(U32^#(isNatList(activate(V))))
                  , isNatIList^#(V) ->
                    c_18(U31^#(isNatIListKind(activate(V)), activate(V)))
                  , U32^#(tt()) -> c_6()
                  , isNatIListKind(n__nil()) -> tt()
                  , isNatIListKind(n__zeros()) -> tt()
                  , isNatIListKind(n__cons(V1, V2)) ->
                    and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                  , isNatIListKind(X) -> n__isNatIListKind(X)
                  , activate(n__zeros()) -> zeros()
                  , activate(n__0()) -> 0()
                  , activate(n__length(X)) -> length(X)
                  , activate(n__s(X)) -> s(X)
                  , activate(n__cons(X1, X2)) -> cons(X1, X2)
                  , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                  , activate(n__nil()) -> nil()
                  , activate(n__and(X1, X2)) -> and(X1, X2)
                  , activate(n__isNatKind(X)) -> isNatKind(X)
                  , activate(X) -> X
                  , zeros() -> cons(0(), n__zeros())
                  , and(tt(), X) -> activate(X)
                  , isNatKind(n__0()) -> tt()
                  , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                  , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                  , length(nil()) -> 0()
                  , length(cons(N, L)) ->
                    U61(and(and(isNatList(activate(L)),
                                n__isNatIListKind(activate(L))),
                            n__and(isNat(N), n__isNatKind(N))),
                        activate(L))
                  , zeros() -> n__zeros()
                  , 0() -> n__0()
                  , length(X) -> n__length(X)
                  , s(X) -> n__s(X)
                  , cons(X1, X2) -> n__cons(X1, X2)
                  , nil() -> n__nil()
                  , and(X1, X2) -> n__and(X1, X2)
                  , isNatKind(X) -> n__isNatKind(X)
                  , U61(tt(), L) -> s(length(activate(L)))
                  , isNat(n__0()) -> tt()
                  , isNat(n__length(V1)) ->
                    U11(isNatIListKind(activate(V1)), activate(V1))
                  , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                  , isNatList(n__nil()) -> tt()
                  , isNatList(n__cons(V1, V2)) ->
                    U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                        activate(V1),
                        activate(V2))
                  , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                  , U21(tt(), V1) -> U22(isNat(activate(V1)))
                  , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                  , U12(tt()) -> tt()
                  , U22(tt()) -> tt()
                  , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                  , U53(tt()) -> tt()}

             Proof Output:
               The input cannot be shown compatible

           * Path {20}: 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(cons) = {}, Uargs(U11) = {}, Uargs(U12) = {},
                 Uargs(isNatList) = {}, Uargs(activate) = {}, Uargs(U21) = {},
                 Uargs(U22) = {}, Uargs(isNat) = {}, Uargs(U31) = {},
                 Uargs(U32) = {}, Uargs(U41) = {}, Uargs(U42) = {}, Uargs(U43) = {},
                 Uargs(isNatIList) = {}, Uargs(U51) = {}, Uargs(U52) = {},
                 Uargs(U53) = {}, Uargs(U61) = {}, Uargs(s) = {},
                 Uargs(length) = {}, Uargs(and) = {}, Uargs(n__length) = {},
                 Uargs(isNatIListKind) = {}, Uargs(n__s) = {},
                 Uargs(isNatKind) = {}, Uargs(n__cons) = {},
                 Uargs(n__isNatIListKind) = {}, Uargs(n__and) = {},
                 Uargs(n__isNatKind) = {}, Uargs(c_0) = {}, Uargs(cons^#) = {},
                 Uargs(U11^#) = {}, Uargs(c_1) = {}, Uargs(U12^#) = {},
                 Uargs(U21^#) = {}, Uargs(c_3) = {}, Uargs(U22^#) = {},
                 Uargs(U31^#) = {}, Uargs(c_5) = {}, Uargs(U32^#) = {},
                 Uargs(U41^#) = {}, Uargs(c_7) = {}, Uargs(U42^#) = {},
                 Uargs(c_8) = {}, Uargs(U43^#) = {}, Uargs(U51^#) = {},
                 Uargs(c_10) = {}, Uargs(U52^#) = {}, Uargs(c_11) = {},
                 Uargs(U53^#) = {}, Uargs(U61^#) = {}, Uargs(c_13) = {},
                 Uargs(s^#) = {}, Uargs(and^#) = {}, Uargs(c_14) = {},
                 Uargs(activate^#) = {}, Uargs(isNat^#) = {}, Uargs(c_16) = {},
                 Uargs(c_17) = {}, Uargs(isNatIList^#) = {}, Uargs(c_18) = {},
                 Uargs(c_20) = {}, Uargs(isNatIListKind^#) = {}, Uargs(c_23) = {},
                 Uargs(isNatKind^#) = {}, Uargs(c_25) = {}, Uargs(c_26) = {},
                 Uargs(isNatList^#) = {}, Uargs(c_28) = {}, Uargs(length^#) = {},
                 Uargs(c_29) = {}, Uargs(c_30) = {}, Uargs(c_40) = {},
                 Uargs(c_41) = {}, Uargs(c_42) = {}, Uargs(c_43) = {},
                 Uargs(c_44) = {}, Uargs(c_45) = {}, Uargs(c_46) = {},
                 Uargs(c_47) = {}, Uargs(c_48) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                zeros() = [0]
                cons(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                n__zeros() = [0]
                U11(x1, x2) = [0] x1 + [0] x2 + [0]
                tt() = [0]
                U12(x1) = [0] x1 + [0]
                isNatList(x1) = [0] x1 + [0]
                activate(x1) = [0] x1 + [0]
                U21(x1, x2) = [0] x1 + [0] x2 + [0]
                U22(x1) = [0] x1 + [0]
                isNat(x1) = [0] x1 + [0]
                U31(x1, x2) = [0] x1 + [0] x2 + [0]
                U32(x1) = [0] x1 + [0]
                U41(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U42(x1, x2) = [0] x1 + [0] x2 + [0]
                U43(x1) = [0] x1 + [0]
                isNatIList(x1) = [0] x1 + [0]
                U51(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U52(x1, x2) = [0] x1 + [0] x2 + [0]
                U53(x1) = [0] x1 + [0]
                U61(x1, x2) = [0] x1 + [0] x2 + [0]
                s(x1) = [0] x1 + [0]
                length(x1) = [0] x1 + [0]
                and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__0() = [0]
                n__length(x1) = [0] x1 + [0]
                isNatIListKind(x1) = [0] x1 + [0]
                n__s(x1) = [0] x1 + [0]
                isNatKind(x1) = [0] x1 + [0]
                n__cons(x1, x2) = [0] x1 + [0] x2 + [0]
                n__isNatIListKind(x1) = [0] x1 + [0]
                n__nil() = [0]
                nil() = [0]
                n__and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__isNatKind(x1) = [0] x1 + [0]
                zeros^#() = [0]
                c_0(x1) = [0] x1 + [0]
                cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
                U11^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_1(x1) = [0] x1 + [0]
                U12^#(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) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                U32^#(x1) = [0] x1 + [0]
                c_6() = [0]
                U41^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_7(x1) = [0] x1 + [0]
                U42^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_8(x1) = [0] x1 + [0]
                U43^#(x1) = [0] x1 + [0]
                c_9() = [0]
                U51^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                U52^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_11(x1) = [0] x1 + [0]
                U53^#(x1) = [0] x1 + [0]
                c_12() = [0]
                U61^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13(x1) = [0] x1 + [0]
                s^#(x1) = [0] x1 + [0]
                and^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_14(x1) = [0] x1 + [0]
                activate^#(x1) = [0] x1 + [0]
                isNat^#(x1) = [0] x1 + [0]
                c_15() = [0]
                c_16(x1) = [0] x1 + [0]
                c_17(x1) = [0] x1 + [0]
                isNatIList^#(x1) = [0] x1 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19() = [0]
                c_20(x1) = [0] x1 + [0]
                isNatIListKind^#(x1) = [0] x1 + [0]
                c_21() = [0]
                c_22() = [0]
                c_23(x1) = [0] x1 + [0]
                isNatKind^#(x1) = [0] x1 + [0]
                c_24() = [0]
                c_25(x1) = [0] x1 + [0]
                c_26(x1) = [0] x1 + [0]
                isNatList^#(x1) = [0] x1 + [0]
                c_27() = [0]
                c_28(x1) = [0] x1 + [0]
                length^#(x1) = [0] x1 + [0]
                c_29(x1) = [0] x1 + [0]
                0^#() = [0]
                c_30(x1) = [0] x1 + [0]
                c_31() = [0]
                c_32() = [0]
                c_33() = [0]
                c_34() = [0]
                c_35() = [0]
                c_36() = [0]
                nil^#() = [0]
                c_37() = [0]
                c_38() = [0]
                c_39() = [0]
                c_40(x1) = [0] x1 + [0]
                c_41(x1) = [0] x1 + [0]
                c_42(x1) = [0] x1 + [0]
                c_43(x1) = [0] x1 + [0]
                c_44(x1) = [0] x1 + [0]
                c_45(x1) = [0] x1 + [0]
                c_46(x1) = [0] x1 + [0]
                c_47(x1) = [0] x1 + [0]
                c_48(x1) = [0] x1 + [0]
                c_49() = [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: {isNatIList^#(n__zeros()) -> c_19()}
               Weak Rules: {}

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

           * Path {21}: inherited
             --------------------

             This path is subsumed by the proof of path {21}->{8}->{9}->{10}.

           * Path {21}->{8}: inherited
             -------------------------

             This path is subsumed by the proof of path {21}->{8}->{9}->{10}.

           * Path {21}->{8}->{9}: inherited
             ------------------------------

             This path is subsumed by the proof of path {21}->{8}->{9}->{10}.

           * Path {21}->{8}->{9}->{10}: NA
             -----------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , and(X1, X2) -> n__and(X1, X2)
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(tt()) -> tt()
                , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V))
                , isNatIList(n__zeros()) -> tt()
                , isNatIList(n__cons(V1, V2)) ->
                  U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U31(tt(), V) -> U32(isNatList(activate(V)))
                , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2))
                , U32(tt()) -> tt()
                , U42(tt(), V2) -> U43(isNatIList(activate(V2)))
                , U43(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 {28}: 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(cons) = {}, Uargs(U11) = {}, Uargs(U12) = {},
                 Uargs(isNatList) = {}, Uargs(activate) = {}, Uargs(U21) = {},
                 Uargs(U22) = {}, Uargs(isNat) = {}, Uargs(U31) = {},
                 Uargs(U32) = {}, Uargs(U41) = {}, Uargs(U42) = {}, Uargs(U43) = {},
                 Uargs(isNatIList) = {}, Uargs(U51) = {}, Uargs(U52) = {},
                 Uargs(U53) = {}, Uargs(U61) = {}, Uargs(s) = {},
                 Uargs(length) = {}, Uargs(and) = {}, Uargs(n__length) = {},
                 Uargs(isNatIListKind) = {}, Uargs(n__s) = {},
                 Uargs(isNatKind) = {}, Uargs(n__cons) = {},
                 Uargs(n__isNatIListKind) = {}, Uargs(n__and) = {},
                 Uargs(n__isNatKind) = {}, Uargs(c_0) = {}, Uargs(cons^#) = {},
                 Uargs(U11^#) = {}, Uargs(c_1) = {}, Uargs(U12^#) = {},
                 Uargs(U21^#) = {}, Uargs(c_3) = {}, Uargs(U22^#) = {},
                 Uargs(U31^#) = {}, Uargs(c_5) = {}, Uargs(U32^#) = {},
                 Uargs(U41^#) = {}, Uargs(c_7) = {}, Uargs(U42^#) = {},
                 Uargs(c_8) = {}, Uargs(U43^#) = {}, Uargs(U51^#) = {},
                 Uargs(c_10) = {}, Uargs(U52^#) = {}, Uargs(c_11) = {},
                 Uargs(U53^#) = {}, Uargs(U61^#) = {}, Uargs(c_13) = {},
                 Uargs(s^#) = {}, Uargs(and^#) = {}, Uargs(c_14) = {},
                 Uargs(activate^#) = {}, Uargs(isNat^#) = {}, Uargs(c_16) = {},
                 Uargs(c_17) = {}, Uargs(isNatIList^#) = {}, Uargs(c_18) = {},
                 Uargs(c_20) = {}, Uargs(isNatIListKind^#) = {}, Uargs(c_23) = {},
                 Uargs(isNatKind^#) = {}, Uargs(c_25) = {}, Uargs(c_26) = {},
                 Uargs(isNatList^#) = {}, Uargs(c_28) = {}, Uargs(length^#) = {},
                 Uargs(c_29) = {}, Uargs(c_30) = {}, Uargs(c_40) = {},
                 Uargs(c_41) = {}, Uargs(c_42) = {}, Uargs(c_43) = {},
                 Uargs(c_44) = {}, Uargs(c_45) = {}, Uargs(c_46) = {},
                 Uargs(c_47) = {}, Uargs(c_48) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                zeros() = [0]
                cons(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                n__zeros() = [0]
                U11(x1, x2) = [0] x1 + [0] x2 + [0]
                tt() = [0]
                U12(x1) = [0] x1 + [0]
                isNatList(x1) = [0] x1 + [0]
                activate(x1) = [0] x1 + [0]
                U21(x1, x2) = [0] x1 + [0] x2 + [0]
                U22(x1) = [0] x1 + [0]
                isNat(x1) = [0] x1 + [0]
                U31(x1, x2) = [0] x1 + [0] x2 + [0]
                U32(x1) = [0] x1 + [0]
                U41(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U42(x1, x2) = [0] x1 + [0] x2 + [0]
                U43(x1) = [0] x1 + [0]
                isNatIList(x1) = [0] x1 + [0]
                U51(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U52(x1, x2) = [0] x1 + [0] x2 + [0]
                U53(x1) = [0] x1 + [0]
                U61(x1, x2) = [0] x1 + [0] x2 + [0]
                s(x1) = [0] x1 + [0]
                length(x1) = [0] x1 + [0]
                and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__0() = [0]
                n__length(x1) = [0] x1 + [0]
                isNatIListKind(x1) = [0] x1 + [0]
                n__s(x1) = [0] x1 + [0]
                isNatKind(x1) = [0] x1 + [0]
                n__cons(x1, x2) = [0] x1 + [0] x2 + [0]
                n__isNatIListKind(x1) = [0] x1 + [0]
                n__nil() = [0]
                nil() = [0]
                n__and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__isNatKind(x1) = [0] x1 + [0]
                zeros^#() = [0]
                c_0(x1) = [0] x1 + [0]
                cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
                U11^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_1(x1) = [0] x1 + [0]
                U12^#(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) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                U32^#(x1) = [0] x1 + [0]
                c_6() = [0]
                U41^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_7(x1) = [0] x1 + [0]
                U42^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_8(x1) = [0] x1 + [0]
                U43^#(x1) = [0] x1 + [0]
                c_9() = [0]
                U51^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                U52^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_11(x1) = [0] x1 + [0]
                U53^#(x1) = [0] x1 + [0]
                c_12() = [0]
                U61^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13(x1) = [0] x1 + [0]
                s^#(x1) = [0] x1 + [0]
                and^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_14(x1) = [0] x1 + [0]
                activate^#(x1) = [0] x1 + [0]
                isNat^#(x1) = [0] x1 + [0]
                c_15() = [0]
                c_16(x1) = [0] x1 + [0]
                c_17(x1) = [0] x1 + [0]
                isNatIList^#(x1) = [0] x1 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19() = [0]
                c_20(x1) = [0] x1 + [0]
                isNatIListKind^#(x1) = [0] x1 + [0]
                c_21() = [0]
                c_22() = [0]
                c_23(x1) = [0] x1 + [0]
                isNatKind^#(x1) = [0] x1 + [0]
                c_24() = [0]
                c_25(x1) = [0] x1 + [0]
                c_26(x1) = [0] x1 + [0]
                isNatList^#(x1) = [0] x1 + [0]
                c_27() = [0]
                c_28(x1) = [0] x1 + [0]
                length^#(x1) = [0] x1 + [0]
                c_29(x1) = [0] x1 + [0]
                0^#() = [0]
                c_30(x1) = [0] x1 + [0]
                c_31() = [0]
                c_32() = [0]
                c_33() = [0]
                c_34() = [0]
                c_35() = [0]
                c_36() = [0]
                nil^#() = [0]
                c_37() = [0]
                c_38() = [0]
                c_39() = [0]
                c_40(x1) = [0] x1 + [0]
                c_41(x1) = [0] x1 + [0]
                c_42(x1) = [0] x1 + [0]
                c_43(x1) = [0] x1 + [0]
                c_44(x1) = [0] x1 + [0]
                c_45(x1) = [0] x1 + [0]
                c_46(x1) = [0] x1 + [0]
                c_47(x1) = [0] x1 + [0]
                c_48(x1) = [0] x1 + [0]
                c_49() = [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: {isNatList^#(n__nil()) -> c_27()}
               Weak Rules: {}

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

           * Path {29}: inherited
             --------------------

             This path is subsumed by the proof of path {29}->{11}->{12}->{13}.

           * Path {29}->{11}: inherited
             --------------------------

             This path is subsumed by the proof of path {29}->{11}->{12}->{13}.

           * Path {29}->{11}->{12}: inherited
             --------------------------------

             This path is subsumed by the proof of path {29}->{11}->{12}->{13}.

           * Path {29}->{11}->{12}->{13}: NA
             -------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , and(X1, X2) -> n__and(X1, X2)
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 LengthOfFiniteLists complete Z

stdout:

MAYBE

Tool RC2

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

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    runtime-complexity with respect to
  Rules:
    {  zeros() -> cons(0(), n__zeros())
     , U11(tt(), V1) -> U12(isNatList(activate(V1)))
     , U12(tt()) -> tt()
     , U21(tt(), V1) -> U22(isNat(activate(V1)))
     , U22(tt()) -> tt()
     , U31(tt(), V) -> U32(isNatList(activate(V)))
     , U32(tt()) -> tt()
     , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2))
     , U42(tt(), V2) -> U43(isNatIList(activate(V2)))
     , U43(tt()) -> tt()
     , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
     , U52(tt(), V2) -> U53(isNatList(activate(V2)))
     , U53(tt()) -> tt()
     , U61(tt(), L) -> s(length(activate(L)))
     , and(tt(), X) -> activate(X)
     , isNat(n__0()) -> tt()
     , isNat(n__length(V1)) ->
       U11(isNatIListKind(activate(V1)), activate(V1))
     , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
     , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V))
     , isNatIList(n__zeros()) -> tt()
     , isNatIList(n__cons(V1, V2)) ->
       U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatIListKind(n__nil()) -> tt()
     , isNatIListKind(n__zeros()) -> tt()
     , isNatIListKind(n__cons(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
     , isNatKind(n__0()) -> tt()
     , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
     , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
     , isNatList(n__nil()) -> tt()
     , isNatList(n__cons(V1, V2)) ->
       U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , length(nil()) -> 0()
     , length(cons(N, L)) ->
       U61(and(and(isNatList(activate(L)),
                   n__isNatIListKind(activate(L))),
               n__and(isNat(N), n__isNatKind(N))),
           activate(L))
     , zeros() -> n__zeros()
     , 0() -> n__0()
     , length(X) -> n__length(X)
     , s(X) -> n__s(X)
     , cons(X1, X2) -> n__cons(X1, X2)
     , isNatIListKind(X) -> n__isNatIListKind(X)
     , nil() -> n__nil()
     , and(X1, X2) -> n__and(X1, X2)
     , isNatKind(X) -> n__isNatKind(X)
     , activate(n__zeros()) -> zeros()
     , activate(n__0()) -> 0()
     , activate(n__length(X)) -> length(X)
     , activate(n__s(X)) -> s(X)
     , activate(n__cons(X1, X2)) -> cons(X1, X2)
     , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
     , activate(n__nil()) -> nil()
     , activate(n__and(X1, X2)) -> and(X1, X2)
     , activate(n__isNatKind(X)) -> isNatKind(X)
     , 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: zeros^#() -> c_0(cons^#(0(), n__zeros()))
              , 2: U11^#(tt(), V1) -> c_1(U12^#(isNatList(activate(V1))))
              , 3: U12^#(tt()) -> c_2()
              , 4: U21^#(tt(), V1) -> c_3(U22^#(isNat(activate(V1))))
              , 5: U22^#(tt()) -> c_4()
              , 6: U31^#(tt(), V) -> c_5(U32^#(isNatList(activate(V))))
              , 7: U32^#(tt()) -> c_6()
              , 8: U41^#(tt(), V1, V2) ->
                   c_7(U42^#(isNat(activate(V1)), activate(V2)))
              , 9: U42^#(tt(), V2) -> c_8(U43^#(isNatIList(activate(V2))))
              , 10: U43^#(tt()) -> c_9()
              , 11: U51^#(tt(), V1, V2) ->
                    c_10(U52^#(isNat(activate(V1)), activate(V2)))
              , 12: U52^#(tt(), V2) -> c_11(U53^#(isNatList(activate(V2))))
              , 13: U53^#(tt()) -> c_12()
              , 14: U61^#(tt(), L) -> c_13(s^#(length(activate(L))))
              , 15: and^#(tt(), X) -> c_14(activate^#(X))
              , 16: isNat^#(n__0()) -> c_15()
              , 17: isNat^#(n__length(V1)) ->
                    c_16(U11^#(isNatIListKind(activate(V1)), activate(V1)))
              , 18: isNat^#(n__s(V1)) ->
                    c_17(U21^#(isNatKind(activate(V1)), activate(V1)))
              , 19: isNatIList^#(V) ->
                    c_18(U31^#(isNatIListKind(activate(V)), activate(V)))
              , 20: isNatIList^#(n__zeros()) -> c_19()
              , 21: isNatIList^#(n__cons(V1, V2)) ->
                    c_20(U41^#(and(isNatKind(activate(V1)),
                                   n__isNatIListKind(activate(V2))),
                               activate(V1),
                               activate(V2)))
              , 22: isNatIListKind^#(n__nil()) -> c_21()
              , 23: isNatIListKind^#(n__zeros()) -> c_22()
              , 24: isNatIListKind^#(n__cons(V1, V2)) ->
                    c_23(and^#(isNatKind(activate(V1)),
                               n__isNatIListKind(activate(V2))))
              , 25: isNatKind^#(n__0()) -> c_24()
              , 26: isNatKind^#(n__length(V1)) ->
                    c_25(isNatIListKind^#(activate(V1)))
              , 27: isNatKind^#(n__s(V1)) -> c_26(isNatKind^#(activate(V1)))
              , 28: isNatList^#(n__nil()) -> c_27()
              , 29: isNatList^#(n__cons(V1, V2)) ->
                    c_28(U51^#(and(isNatKind(activate(V1)),
                                   n__isNatIListKind(activate(V2))),
                               activate(V1),
                               activate(V2)))
              , 30: length^#(nil()) -> c_29(0^#())
              , 31: length^#(cons(N, L)) ->
                    c_30(U61^#(and(and(isNatList(activate(L)),
                                       n__isNatIListKind(activate(L))),
                                   n__and(isNat(N), n__isNatKind(N))),
                               activate(L)))
              , 32: zeros^#() -> c_31()
              , 33: 0^#() -> c_32()
              , 34: length^#(X) -> c_33(X)
              , 35: s^#(X) -> c_34(X)
              , 36: cons^#(X1, X2) -> c_35(X1, X2)
              , 37: isNatIListKind^#(X) -> c_36(X)
              , 38: nil^#() -> c_37()
              , 39: and^#(X1, X2) -> c_38(X1, X2)
              , 40: isNatKind^#(X) -> c_39(X)
              , 41: activate^#(n__zeros()) -> c_40(zeros^#())
              , 42: activate^#(n__0()) -> c_41(0^#())
              , 43: activate^#(n__length(X)) -> c_42(length^#(X))
              , 44: activate^#(n__s(X)) -> c_43(s^#(X))
              , 45: activate^#(n__cons(X1, X2)) -> c_44(cons^#(X1, X2))
              , 46: activate^#(n__isNatIListKind(X)) -> c_45(isNatIListKind^#(X))
              , 47: activate^#(n__nil()) -> c_46(nil^#())
              , 48: activate^#(n__and(X1, X2)) -> c_47(and^#(X1, X2))
              , 49: activate^#(n__isNatKind(X)) -> c_48(isNatKind^#(X))
              , 50: activate^#(X) -> c_49(X)}

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

             ->{29}                                                      [     inherited      ]
                |
                `->{11}                                                  [     inherited      ]
                    |
                    `->{12}                                              [     inherited      ]
                        |
                        `->{13}                                          [         NA         ]

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

             ->{21}                                                      [     inherited      ]
                |
                `->{8}                                                   [     inherited      ]
                    |
                    `->{9}                                               [     inherited      ]
                        |
                        `->{10}                                          [         NA         ]

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

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

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

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

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

             ->{15,48,24,46,26,49,27}                                    [     inherited      ]
                |
                |->{22}                                                  [         NA         ]
                |
                |->{23}                                                  [         NA         ]
                |
                |->{25}                                                  [         NA         ]
                |
                |->{37}                                                  [         NA         ]
                |
                |->{39}                                                  [         NA         ]
                |
                |->{40}                                                  [         NA         ]
                |
                |->{41}                                                  [     inherited      ]
                |   |
                |   |->{1}                                               [     inherited      ]
                |   |   |
                |   |   `->{36}                                          [         NA         ]
                |   |
                |   `->{32}                                              [         NA         ]
                |
                |->{42}                                                  [     inherited      ]
                |   |
                |   `->{33}                                              [         NA         ]
                |
                |->{43}                                                  [     inherited      ]
                |   |
                |   |->{30}                                              [     inherited      ]
                |   |   |
                |   |   `->{33}                                          [         NA         ]
                |   |
                |   |->{31}                                              [     inherited      ]
                |   |   |
                |   |   `->{14}                                          [     inherited      ]
                |   |       |
                |   |       `->{35}                                      [         NA         ]
                |   |
                |   `->{34}                                              [         NA         ]
                |
                |->{44}                                                  [     inherited      ]
                |   |
                |   `->{35}                                              [         NA         ]
                |
                |->{45}                                                  [     inherited      ]
                |   |
                |   `->{36}                                              [         NA         ]
                |
                |->{47}                                                  [     inherited      ]
                |   |
                |   `->{38}                                              [         NA         ]
                |
                `->{50}                                                  [         NA         ]



         Sub-problems:
         -------------
           * Path {15,48,24,46,26,49,27}: inherited
             --------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{47}->{38}.

           * Path {15,48,24,46,26,49,27}->{22}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{23}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{25}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{37}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{39}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{40}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{41}: inherited
             --------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{41}->{1}->{36}.

           * Path {15,48,24,46,26,49,27}->{41}->{1}: inherited
             -------------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{41}->{1}->{36}.

           * Path {15,48,24,46,26,49,27}->{41}->{1}->{36}: NA
             ------------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{41}->{32}: NA
             -------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{42}: inherited
             --------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{42}->{33}.

           * Path {15,48,24,46,26,49,27}->{42}->{33}: NA
             -------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{43}: inherited
             --------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{43}->{31}->{14}->{35}.

           * Path {15,48,24,46,26,49,27}->{43}->{30}: inherited
             --------------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{43}->{30}->{33}.

           * Path {15,48,24,46,26,49,27}->{43}->{30}->{33}: NA
             -------------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{43}->{31}: inherited
             --------------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{43}->{31}->{14}->{35}.

           * Path {15,48,24,46,26,49,27}->{43}->{31}->{14}: inherited
             --------------------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{43}->{31}->{14}->{35}.

           * Path {15,48,24,46,26,49,27}->{43}->{31}->{14}->{35}: NA
             -------------------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{43}->{34}: NA
             -------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{44}: inherited
             --------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{44}->{35}.

           * Path {15,48,24,46,26,49,27}->{44}->{35}: NA
             -------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{45}: inherited
             --------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{45}->{36}.

           * Path {15,48,24,46,26,49,27}->{45}->{36}: NA
             -------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{47}: inherited
             --------------------------------------------

             This path is subsumed by the proof of path {15,48,24,46,26,49,27}->{47}->{38}.

           * Path {15,48,24,46,26,49,27}->{47}->{38}: NA
             -------------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {15,48,24,46,26,49,27}->{50}: NA
             -------------------------------------

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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}: 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(cons) = {}, Uargs(U11) = {}, Uargs(U12) = {},
                 Uargs(isNatList) = {}, Uargs(activate) = {}, Uargs(U21) = {},
                 Uargs(U22) = {}, Uargs(isNat) = {}, Uargs(U31) = {},
                 Uargs(U32) = {}, Uargs(U41) = {}, Uargs(U42) = {}, Uargs(U43) = {},
                 Uargs(isNatIList) = {}, Uargs(U51) = {}, Uargs(U52) = {},
                 Uargs(U53) = {}, Uargs(U61) = {}, Uargs(s) = {},
                 Uargs(length) = {}, Uargs(and) = {}, Uargs(n__length) = {},
                 Uargs(isNatIListKind) = {}, Uargs(n__s) = {},
                 Uargs(isNatKind) = {}, Uargs(n__cons) = {},
                 Uargs(n__isNatIListKind) = {}, Uargs(n__and) = {},
                 Uargs(n__isNatKind) = {}, Uargs(c_0) = {}, Uargs(cons^#) = {},
                 Uargs(U11^#) = {}, Uargs(c_1) = {}, Uargs(U12^#) = {},
                 Uargs(U21^#) = {}, Uargs(c_3) = {}, Uargs(U22^#) = {},
                 Uargs(U31^#) = {}, Uargs(c_5) = {}, Uargs(U32^#) = {},
                 Uargs(U41^#) = {}, Uargs(c_7) = {}, Uargs(U42^#) = {},
                 Uargs(c_8) = {}, Uargs(U43^#) = {}, Uargs(U51^#) = {},
                 Uargs(c_10) = {}, Uargs(U52^#) = {}, Uargs(c_11) = {},
                 Uargs(U53^#) = {}, Uargs(U61^#) = {}, Uargs(c_13) = {},
                 Uargs(s^#) = {}, Uargs(and^#) = {}, Uargs(c_14) = {},
                 Uargs(activate^#) = {}, Uargs(isNat^#) = {}, Uargs(c_16) = {},
                 Uargs(c_17) = {}, Uargs(isNatIList^#) = {}, Uargs(c_18) = {},
                 Uargs(c_20) = {}, Uargs(isNatIListKind^#) = {}, Uargs(c_23) = {},
                 Uargs(isNatKind^#) = {}, Uargs(c_25) = {}, Uargs(c_26) = {},
                 Uargs(isNatList^#) = {}, Uargs(c_28) = {}, Uargs(length^#) = {},
                 Uargs(c_29) = {}, Uargs(c_30) = {}, Uargs(c_33) = {},
                 Uargs(c_34) = {}, Uargs(c_35) = {}, Uargs(c_36) = {},
                 Uargs(c_38) = {}, Uargs(c_39) = {}, Uargs(c_40) = {},
                 Uargs(c_41) = {}, Uargs(c_42) = {}, Uargs(c_43) = {},
                 Uargs(c_44) = {}, Uargs(c_45) = {}, Uargs(c_46) = {},
                 Uargs(c_47) = {}, Uargs(c_48) = {}, Uargs(c_49) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                zeros() = [0]
                cons(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                n__zeros() = [0]
                U11(x1, x2) = [0] x1 + [0] x2 + [0]
                tt() = [0]
                U12(x1) = [0] x1 + [0]
                isNatList(x1) = [0] x1 + [0]
                activate(x1) = [0] x1 + [0]
                U21(x1, x2) = [0] x1 + [0] x2 + [0]
                U22(x1) = [0] x1 + [0]
                isNat(x1) = [0] x1 + [0]
                U31(x1, x2) = [0] x1 + [0] x2 + [0]
                U32(x1) = [0] x1 + [0]
                U41(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U42(x1, x2) = [0] x1 + [0] x2 + [0]
                U43(x1) = [0] x1 + [0]
                isNatIList(x1) = [0] x1 + [0]
                U51(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U52(x1, x2) = [0] x1 + [0] x2 + [0]
                U53(x1) = [0] x1 + [0]
                U61(x1, x2) = [0] x1 + [0] x2 + [0]
                s(x1) = [0] x1 + [0]
                length(x1) = [0] x1 + [0]
                and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__0() = [0]
                n__length(x1) = [0] x1 + [0]
                isNatIListKind(x1) = [0] x1 + [0]
                n__s(x1) = [0] x1 + [0]
                isNatKind(x1) = [0] x1 + [0]
                n__cons(x1, x2) = [0] x1 + [0] x2 + [0]
                n__isNatIListKind(x1) = [0] x1 + [0]
                n__nil() = [0]
                nil() = [0]
                n__and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__isNatKind(x1) = [0] x1 + [0]
                zeros^#() = [0]
                c_0(x1) = [0] x1 + [0]
                cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
                U11^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_1(x1) = [0] x1 + [0]
                U12^#(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) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                U32^#(x1) = [0] x1 + [0]
                c_6() = [0]
                U41^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_7(x1) = [0] x1 + [0]
                U42^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_8(x1) = [0] x1 + [0]
                U43^#(x1) = [0] x1 + [0]
                c_9() = [0]
                U51^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                U52^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_11(x1) = [0] x1 + [0]
                U53^#(x1) = [0] x1 + [0]
                c_12() = [0]
                U61^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13(x1) = [0] x1 + [0]
                s^#(x1) = [0] x1 + [0]
                and^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_14(x1) = [0] x1 + [0]
                activate^#(x1) = [0] x1 + [0]
                isNat^#(x1) = [0] x1 + [0]
                c_15() = [0]
                c_16(x1) = [0] x1 + [0]
                c_17(x1) = [0] x1 + [0]
                isNatIList^#(x1) = [0] x1 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19() = [0]
                c_20(x1) = [0] x1 + [0]
                isNatIListKind^#(x1) = [0] x1 + [0]
                c_21() = [0]
                c_22() = [0]
                c_23(x1) = [0] x1 + [0]
                isNatKind^#(x1) = [0] x1 + [0]
                c_24() = [0]
                c_25(x1) = [0] x1 + [0]
                c_26(x1) = [0] x1 + [0]
                isNatList^#(x1) = [0] x1 + [0]
                c_27() = [0]
                c_28(x1) = [0] x1 + [0]
                length^#(x1) = [0] x1 + [0]
                c_29(x1) = [0] x1 + [0]
                0^#() = [0]
                c_30(x1) = [0] x1 + [0]
                c_31() = [0]
                c_32() = [0]
                c_33(x1) = [0] x1 + [0]
                c_34(x1) = [0] x1 + [0]
                c_35(x1, x2) = [0] x1 + [0] x2 + [0]
                c_36(x1) = [0] x1 + [0]
                nil^#() = [0]
                c_37() = [0]
                c_38(x1, x2) = [0] x1 + [0] x2 + [0]
                c_39(x1) = [0] x1 + [0]
                c_40(x1) = [0] x1 + [0]
                c_41(x1) = [0] x1 + [0]
                c_42(x1) = [0] x1 + [0]
                c_43(x1) = [0] x1 + [0]
                c_44(x1) = [0] x1 + [0]
                c_45(x1) = [0] x1 + [0]
                c_46(x1) = [0] x1 + [0]
                c_47(x1) = [0] x1 + [0]
                c_48(x1) = [0] x1 + [0]
                c_49(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_15()}
               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_15() = [1]

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

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

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

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

           * Path {17}->{2}->{3}: NA
             -----------------------

             The usable rules for this path are:

               {  isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , isNatKind(X) -> n__isNatKind(X)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {18}: inherited
             --------------------

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

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

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

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

             The usable rules for this path are:

               {  isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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_17(U21^#(isNatKind(activate(V1)), activate(V1)))
                  , U22^#(tt()) -> c_4()
                  , isNatKind(n__0()) -> tt()
                  , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                  , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                  , isNatKind(X) -> n__isNatKind(X)
                  , activate(n__zeros()) -> zeros()
                  , activate(n__0()) -> 0()
                  , activate(n__length(X)) -> length(X)
                  , activate(n__s(X)) -> s(X)
                  , activate(n__cons(X1, X2)) -> cons(X1, X2)
                  , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                  , activate(n__nil()) -> nil()
                  , activate(n__and(X1, X2)) -> and(X1, X2)
                  , activate(n__isNatKind(X)) -> isNatKind(X)
                  , activate(X) -> X
                  , zeros() -> cons(0(), n__zeros())
                  , and(tt(), X) -> activate(X)
                  , isNatIListKind(n__nil()) -> tt()
                  , isNatIListKind(n__zeros()) -> tt()
                  , isNatIListKind(n__cons(V1, V2)) ->
                    and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                  , length(nil()) -> 0()
                  , length(cons(N, L)) ->
                    U61(and(and(isNatList(activate(L)),
                                n__isNatIListKind(activate(L))),
                            n__and(isNat(N), n__isNatKind(N))),
                        activate(L))
                  , zeros() -> n__zeros()
                  , 0() -> n__0()
                  , length(X) -> n__length(X)
                  , s(X) -> n__s(X)
                  , cons(X1, X2) -> n__cons(X1, X2)
                  , isNatIListKind(X) -> n__isNatIListKind(X)
                  , nil() -> n__nil()
                  , and(X1, X2) -> n__and(X1, X2)
                  , U61(tt(), L) -> s(length(activate(L)))
                  , isNat(n__0()) -> tt()
                  , isNat(n__length(V1)) ->
                    U11(isNatIListKind(activate(V1)), activate(V1))
                  , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                  , isNatList(n__nil()) -> tt()
                  , isNatList(n__cons(V1, V2)) ->
                    U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                        activate(V1),
                        activate(V2))
                  , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                  , U21(tt(), V1) -> U22(isNat(activate(V1)))
                  , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                  , U12(tt()) -> tt()
                  , U22(tt()) -> tt()
                  , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                  , U53(tt()) -> tt()}

             Proof Output:
               The input cannot be shown compatible

           * Path {19}: inherited
             --------------------

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

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

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

           * Path {19}->{6}->{7}: NA
             -----------------------

             The usable rules for this path are:

               {  isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , and(tt(), X) -> activate(X)
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , nil() -> n__nil()
                , and(X1, X2) -> n__and(X1, X2)
                , isNatKind(X) -> n__isNatKind(X)
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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 {20}: 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(cons) = {}, Uargs(U11) = {}, Uargs(U12) = {},
                 Uargs(isNatList) = {}, Uargs(activate) = {}, Uargs(U21) = {},
                 Uargs(U22) = {}, Uargs(isNat) = {}, Uargs(U31) = {},
                 Uargs(U32) = {}, Uargs(U41) = {}, Uargs(U42) = {}, Uargs(U43) = {},
                 Uargs(isNatIList) = {}, Uargs(U51) = {}, Uargs(U52) = {},
                 Uargs(U53) = {}, Uargs(U61) = {}, Uargs(s) = {},
                 Uargs(length) = {}, Uargs(and) = {}, Uargs(n__length) = {},
                 Uargs(isNatIListKind) = {}, Uargs(n__s) = {},
                 Uargs(isNatKind) = {}, Uargs(n__cons) = {},
                 Uargs(n__isNatIListKind) = {}, Uargs(n__and) = {},
                 Uargs(n__isNatKind) = {}, Uargs(c_0) = {}, Uargs(cons^#) = {},
                 Uargs(U11^#) = {}, Uargs(c_1) = {}, Uargs(U12^#) = {},
                 Uargs(U21^#) = {}, Uargs(c_3) = {}, Uargs(U22^#) = {},
                 Uargs(U31^#) = {}, Uargs(c_5) = {}, Uargs(U32^#) = {},
                 Uargs(U41^#) = {}, Uargs(c_7) = {}, Uargs(U42^#) = {},
                 Uargs(c_8) = {}, Uargs(U43^#) = {}, Uargs(U51^#) = {},
                 Uargs(c_10) = {}, Uargs(U52^#) = {}, Uargs(c_11) = {},
                 Uargs(U53^#) = {}, Uargs(U61^#) = {}, Uargs(c_13) = {},
                 Uargs(s^#) = {}, Uargs(and^#) = {}, Uargs(c_14) = {},
                 Uargs(activate^#) = {}, Uargs(isNat^#) = {}, Uargs(c_16) = {},
                 Uargs(c_17) = {}, Uargs(isNatIList^#) = {}, Uargs(c_18) = {},
                 Uargs(c_20) = {}, Uargs(isNatIListKind^#) = {}, Uargs(c_23) = {},
                 Uargs(isNatKind^#) = {}, Uargs(c_25) = {}, Uargs(c_26) = {},
                 Uargs(isNatList^#) = {}, Uargs(c_28) = {}, Uargs(length^#) = {},
                 Uargs(c_29) = {}, Uargs(c_30) = {}, Uargs(c_33) = {},
                 Uargs(c_34) = {}, Uargs(c_35) = {}, Uargs(c_36) = {},
                 Uargs(c_38) = {}, Uargs(c_39) = {}, Uargs(c_40) = {},
                 Uargs(c_41) = {}, Uargs(c_42) = {}, Uargs(c_43) = {},
                 Uargs(c_44) = {}, Uargs(c_45) = {}, Uargs(c_46) = {},
                 Uargs(c_47) = {}, Uargs(c_48) = {}, Uargs(c_49) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                zeros() = [0]
                cons(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                n__zeros() = [0]
                U11(x1, x2) = [0] x1 + [0] x2 + [0]
                tt() = [0]
                U12(x1) = [0] x1 + [0]
                isNatList(x1) = [0] x1 + [0]
                activate(x1) = [0] x1 + [0]
                U21(x1, x2) = [0] x1 + [0] x2 + [0]
                U22(x1) = [0] x1 + [0]
                isNat(x1) = [0] x1 + [0]
                U31(x1, x2) = [0] x1 + [0] x2 + [0]
                U32(x1) = [0] x1 + [0]
                U41(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U42(x1, x2) = [0] x1 + [0] x2 + [0]
                U43(x1) = [0] x1 + [0]
                isNatIList(x1) = [0] x1 + [0]
                U51(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U52(x1, x2) = [0] x1 + [0] x2 + [0]
                U53(x1) = [0] x1 + [0]
                U61(x1, x2) = [0] x1 + [0] x2 + [0]
                s(x1) = [0] x1 + [0]
                length(x1) = [0] x1 + [0]
                and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__0() = [0]
                n__length(x1) = [0] x1 + [0]
                isNatIListKind(x1) = [0] x1 + [0]
                n__s(x1) = [0] x1 + [0]
                isNatKind(x1) = [0] x1 + [0]
                n__cons(x1, x2) = [0] x1 + [0] x2 + [0]
                n__isNatIListKind(x1) = [0] x1 + [0]
                n__nil() = [0]
                nil() = [0]
                n__and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__isNatKind(x1) = [0] x1 + [0]
                zeros^#() = [0]
                c_0(x1) = [0] x1 + [0]
                cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
                U11^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_1(x1) = [0] x1 + [0]
                U12^#(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) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                U32^#(x1) = [0] x1 + [0]
                c_6() = [0]
                U41^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_7(x1) = [0] x1 + [0]
                U42^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_8(x1) = [0] x1 + [0]
                U43^#(x1) = [0] x1 + [0]
                c_9() = [0]
                U51^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                U52^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_11(x1) = [0] x1 + [0]
                U53^#(x1) = [0] x1 + [0]
                c_12() = [0]
                U61^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13(x1) = [0] x1 + [0]
                s^#(x1) = [0] x1 + [0]
                and^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_14(x1) = [0] x1 + [0]
                activate^#(x1) = [0] x1 + [0]
                isNat^#(x1) = [0] x1 + [0]
                c_15() = [0]
                c_16(x1) = [0] x1 + [0]
                c_17(x1) = [0] x1 + [0]
                isNatIList^#(x1) = [0] x1 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19() = [0]
                c_20(x1) = [0] x1 + [0]
                isNatIListKind^#(x1) = [0] x1 + [0]
                c_21() = [0]
                c_22() = [0]
                c_23(x1) = [0] x1 + [0]
                isNatKind^#(x1) = [0] x1 + [0]
                c_24() = [0]
                c_25(x1) = [0] x1 + [0]
                c_26(x1) = [0] x1 + [0]
                isNatList^#(x1) = [0] x1 + [0]
                c_27() = [0]
                c_28(x1) = [0] x1 + [0]
                length^#(x1) = [0] x1 + [0]
                c_29(x1) = [0] x1 + [0]
                0^#() = [0]
                c_30(x1) = [0] x1 + [0]
                c_31() = [0]
                c_32() = [0]
                c_33(x1) = [0] x1 + [0]
                c_34(x1) = [0] x1 + [0]
                c_35(x1, x2) = [0] x1 + [0] x2 + [0]
                c_36(x1) = [0] x1 + [0]
                nil^#() = [0]
                c_37() = [0]
                c_38(x1, x2) = [0] x1 + [0] x2 + [0]
                c_39(x1) = [0] x1 + [0]
                c_40(x1) = [0] x1 + [0]
                c_41(x1) = [0] x1 + [0]
                c_42(x1) = [0] x1 + [0]
                c_43(x1) = [0] x1 + [0]
                c_44(x1) = [0] x1 + [0]
                c_45(x1) = [0] x1 + [0]
                c_46(x1) = [0] x1 + [0]
                c_47(x1) = [0] x1 + [0]
                c_48(x1) = [0] x1 + [0]
                c_49(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: {isNatIList^#(n__zeros()) -> c_19()}
               Weak Rules: {}

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

           * Path {21}: inherited
             --------------------

             This path is subsumed by the proof of path {21}->{8}->{9}->{10}.

           * Path {21}->{8}: inherited
             -------------------------

             This path is subsumed by the proof of path {21}->{8}->{9}->{10}.

           * Path {21}->{8}->{9}: inherited
             ------------------------------

             This path is subsumed by the proof of path {21}->{8}->{9}->{10}.

           * Path {21}->{8}->{9}->{10}: NA
             -----------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , and(X1, X2) -> n__and(X1, X2)
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(tt()) -> tt()
                , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V))
                , isNatIList(n__zeros()) -> tt()
                , isNatIList(n__cons(V1, V2)) ->
                  U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U31(tt(), V) -> U32(isNatList(activate(V)))
                , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2))
                , U32(tt()) -> tt()
                , U42(tt(), V2) -> U43(isNatIList(activate(V2)))
                , U43(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 {28}: 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(cons) = {}, Uargs(U11) = {}, Uargs(U12) = {},
                 Uargs(isNatList) = {}, Uargs(activate) = {}, Uargs(U21) = {},
                 Uargs(U22) = {}, Uargs(isNat) = {}, Uargs(U31) = {},
                 Uargs(U32) = {}, Uargs(U41) = {}, Uargs(U42) = {}, Uargs(U43) = {},
                 Uargs(isNatIList) = {}, Uargs(U51) = {}, Uargs(U52) = {},
                 Uargs(U53) = {}, Uargs(U61) = {}, Uargs(s) = {},
                 Uargs(length) = {}, Uargs(and) = {}, Uargs(n__length) = {},
                 Uargs(isNatIListKind) = {}, Uargs(n__s) = {},
                 Uargs(isNatKind) = {}, Uargs(n__cons) = {},
                 Uargs(n__isNatIListKind) = {}, Uargs(n__and) = {},
                 Uargs(n__isNatKind) = {}, Uargs(c_0) = {}, Uargs(cons^#) = {},
                 Uargs(U11^#) = {}, Uargs(c_1) = {}, Uargs(U12^#) = {},
                 Uargs(U21^#) = {}, Uargs(c_3) = {}, Uargs(U22^#) = {},
                 Uargs(U31^#) = {}, Uargs(c_5) = {}, Uargs(U32^#) = {},
                 Uargs(U41^#) = {}, Uargs(c_7) = {}, Uargs(U42^#) = {},
                 Uargs(c_8) = {}, Uargs(U43^#) = {}, Uargs(U51^#) = {},
                 Uargs(c_10) = {}, Uargs(U52^#) = {}, Uargs(c_11) = {},
                 Uargs(U53^#) = {}, Uargs(U61^#) = {}, Uargs(c_13) = {},
                 Uargs(s^#) = {}, Uargs(and^#) = {}, Uargs(c_14) = {},
                 Uargs(activate^#) = {}, Uargs(isNat^#) = {}, Uargs(c_16) = {},
                 Uargs(c_17) = {}, Uargs(isNatIList^#) = {}, Uargs(c_18) = {},
                 Uargs(c_20) = {}, Uargs(isNatIListKind^#) = {}, Uargs(c_23) = {},
                 Uargs(isNatKind^#) = {}, Uargs(c_25) = {}, Uargs(c_26) = {},
                 Uargs(isNatList^#) = {}, Uargs(c_28) = {}, Uargs(length^#) = {},
                 Uargs(c_29) = {}, Uargs(c_30) = {}, Uargs(c_33) = {},
                 Uargs(c_34) = {}, Uargs(c_35) = {}, Uargs(c_36) = {},
                 Uargs(c_38) = {}, Uargs(c_39) = {}, Uargs(c_40) = {},
                 Uargs(c_41) = {}, Uargs(c_42) = {}, Uargs(c_43) = {},
                 Uargs(c_44) = {}, Uargs(c_45) = {}, Uargs(c_46) = {},
                 Uargs(c_47) = {}, Uargs(c_48) = {}, Uargs(c_49) = {}
               We have the following constructor-restricted matrix interpretation:
               Interpretation Functions:
                zeros() = [0]
                cons(x1, x2) = [0] x1 + [0] x2 + [0]
                0() = [0]
                n__zeros() = [0]
                U11(x1, x2) = [0] x1 + [0] x2 + [0]
                tt() = [0]
                U12(x1) = [0] x1 + [0]
                isNatList(x1) = [0] x1 + [0]
                activate(x1) = [0] x1 + [0]
                U21(x1, x2) = [0] x1 + [0] x2 + [0]
                U22(x1) = [0] x1 + [0]
                isNat(x1) = [0] x1 + [0]
                U31(x1, x2) = [0] x1 + [0] x2 + [0]
                U32(x1) = [0] x1 + [0]
                U41(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U42(x1, x2) = [0] x1 + [0] x2 + [0]
                U43(x1) = [0] x1 + [0]
                isNatIList(x1) = [0] x1 + [0]
                U51(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                U52(x1, x2) = [0] x1 + [0] x2 + [0]
                U53(x1) = [0] x1 + [0]
                U61(x1, x2) = [0] x1 + [0] x2 + [0]
                s(x1) = [0] x1 + [0]
                length(x1) = [0] x1 + [0]
                and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__0() = [0]
                n__length(x1) = [0] x1 + [0]
                isNatIListKind(x1) = [0] x1 + [0]
                n__s(x1) = [0] x1 + [0]
                isNatKind(x1) = [0] x1 + [0]
                n__cons(x1, x2) = [0] x1 + [0] x2 + [0]
                n__isNatIListKind(x1) = [0] x1 + [0]
                n__nil() = [0]
                nil() = [0]
                n__and(x1, x2) = [0] x1 + [0] x2 + [0]
                n__isNatKind(x1) = [0] x1 + [0]
                zeros^#() = [0]
                c_0(x1) = [0] x1 + [0]
                cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
                U11^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_1(x1) = [0] x1 + [0]
                U12^#(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) = [0] x1 + [0] x2 + [0]
                c_5(x1) = [0] x1 + [0]
                U32^#(x1) = [0] x1 + [0]
                c_6() = [0]
                U41^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_7(x1) = [0] x1 + [0]
                U42^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_8(x1) = [0] x1 + [0]
                U43^#(x1) = [0] x1 + [0]
                c_9() = [0]
                U51^#(x1, x2, x3) = [0] x1 + [0] x2 + [0] x3 + [0]
                c_10(x1) = [0] x1 + [0]
                U52^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_11(x1) = [0] x1 + [0]
                U53^#(x1) = [0] x1 + [0]
                c_12() = [0]
                U61^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_13(x1) = [0] x1 + [0]
                s^#(x1) = [0] x1 + [0]
                and^#(x1, x2) = [0] x1 + [0] x2 + [0]
                c_14(x1) = [0] x1 + [0]
                activate^#(x1) = [0] x1 + [0]
                isNat^#(x1) = [0] x1 + [0]
                c_15() = [0]
                c_16(x1) = [0] x1 + [0]
                c_17(x1) = [0] x1 + [0]
                isNatIList^#(x1) = [0] x1 + [0]
                c_18(x1) = [0] x1 + [0]
                c_19() = [0]
                c_20(x1) = [0] x1 + [0]
                isNatIListKind^#(x1) = [0] x1 + [0]
                c_21() = [0]
                c_22() = [0]
                c_23(x1) = [0] x1 + [0]
                isNatKind^#(x1) = [0] x1 + [0]
                c_24() = [0]
                c_25(x1) = [0] x1 + [0]
                c_26(x1) = [0] x1 + [0]
                isNatList^#(x1) = [0] x1 + [0]
                c_27() = [0]
                c_28(x1) = [0] x1 + [0]
                length^#(x1) = [0] x1 + [0]
                c_29(x1) = [0] x1 + [0]
                0^#() = [0]
                c_30(x1) = [0] x1 + [0]
                c_31() = [0]
                c_32() = [0]
                c_33(x1) = [0] x1 + [0]
                c_34(x1) = [0] x1 + [0]
                c_35(x1, x2) = [0] x1 + [0] x2 + [0]
                c_36(x1) = [0] x1 + [0]
                nil^#() = [0]
                c_37() = [0]
                c_38(x1, x2) = [0] x1 + [0] x2 + [0]
                c_39(x1) = [0] x1 + [0]
                c_40(x1) = [0] x1 + [0]
                c_41(x1) = [0] x1 + [0]
                c_42(x1) = [0] x1 + [0]
                c_43(x1) = [0] x1 + [0]
                c_44(x1) = [0] x1 + [0]
                c_45(x1) = [0] x1 + [0]
                c_46(x1) = [0] x1 + [0]
                c_47(x1) = [0] x1 + [0]
                c_48(x1) = [0] x1 + [0]
                c_49(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: {isNatList^#(n__nil()) -> c_27()}
               Weak Rules: {}

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

           * Path {29}: inherited
             --------------------

             This path is subsumed by the proof of path {29}->{11}->{12}->{13}.

           * Path {29}->{11}: inherited
             --------------------------

             This path is subsumed by the proof of path {29}->{11}->{12}->{13}.

           * Path {29}->{11}->{12}: inherited
             --------------------------------

             This path is subsumed by the proof of path {29}->{11}->{12}->{13}.

           * Path {29}->{11}->{12}->{13}: NA
             -------------------------------

             The usable rules for this path are:

               {  and(tt(), X) -> activate(X)
                , isNatKind(n__0()) -> tt()
                , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
                , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
                , and(X1, X2) -> n__and(X1, X2)
                , isNatKind(X) -> n__isNatKind(X)
                , activate(n__zeros()) -> zeros()
                , activate(n__0()) -> 0()
                , activate(n__length(X)) -> length(X)
                , activate(n__s(X)) -> s(X)
                , activate(n__cons(X1, X2)) -> cons(X1, X2)
                , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
                , activate(n__nil()) -> nil()
                , activate(n__and(X1, X2)) -> and(X1, X2)
                , activate(n__isNatKind(X)) -> isNatKind(X)
                , activate(X) -> X
                , zeros() -> cons(0(), n__zeros())
                , isNatIListKind(n__nil()) -> tt()
                , isNatIListKind(n__zeros()) -> tt()
                , isNatIListKind(n__cons(V1, V2)) ->
                  and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
                , length(nil()) -> 0()
                , length(cons(N, L)) ->
                  U61(and(and(isNatList(activate(L)),
                              n__isNatIListKind(activate(L))),
                          n__and(isNat(N), n__isNatKind(N))),
                      activate(L))
                , zeros() -> n__zeros()
                , 0() -> n__0()
                , length(X) -> n__length(X)
                , s(X) -> n__s(X)
                , cons(X1, X2) -> n__cons(X1, X2)
                , isNatIListKind(X) -> n__isNatIListKind(X)
                , nil() -> n__nil()
                , U61(tt(), L) -> s(length(activate(L)))
                , isNat(n__0()) -> tt()
                , isNat(n__length(V1)) ->
                  U11(isNatIListKind(activate(V1)), activate(V1))
                , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
                , isNatList(n__nil()) -> tt()
                , isNatList(n__cons(V1, V2)) ->
                  U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2))
                , U11(tt(), V1) -> U12(isNatList(activate(V1)))
                , U21(tt(), V1) -> U22(isNat(activate(V1)))
                , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
                , U12(tt()) -> tt()
                , U22(tt()) -> tt()
                , U52(tt(), V2) -> U53(isNatList(activate(V2)))
                , U53(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.