- : unit = ()
- : unit = ()
h : heuristic = <heuristic>
- : unit = ()
APPLY CRITERIA (Marked dependency pairs)

TRS termination of:
[1] zeros -> cons(0,n__zeros)
[2] U11(tt,V1) -> U12(isNatList(activate(V1)))
[3] U12(tt) -> tt
[4] U21(tt,V1) -> U22(isNat(activate(V1)))
[5] U22(tt) -> tt
[6] U31(tt,V) -> U32(isNatList(activate(V)))
[7] U32(tt) -> tt
[8] U41(tt,V1,V2) -> U42(isNat(activate(V1)),activate(V2))
[9] U42(tt,V2) -> U43(isNatIList(activate(V2)))
[10] U43(tt) -> tt
[11] U51(tt,V1,V2) -> U52(isNat(activate(V1)),activate(V2))
[12] U52(tt,V2) -> U53(isNatList(activate(V2)))
[13] U53(tt) -> tt
[14] U61(tt,L) -> s(length(activate(L)))
[15] and(tt,X) -> activate(X)
[16] isNat(n__0) -> tt
[17] isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)),activate(V1))
[18] isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
[19] isNatIList(V) -> U31(isNatIListKind(activate(V)),activate(V))
[20] isNatIList(n__zeros) -> tt
[21] isNatIList(n__cons(V1,V2)) ->
 U41(and(isNatKind(activate(V1)),n__isNatIListKind(activate(V2))),activate(V1),
  activate(V2))
[22] isNatIListKind(n__nil) -> tt
[23] isNatIListKind(n__zeros) -> tt
[24] isNatIListKind(n__cons(V1,V2)) ->
 and(isNatKind(activate(V1)),n__isNatIListKind(activate(V2)))
[25] isNatKind(n__0) -> tt
[26] isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
[27] isNatKind(n__s(V1)) -> isNatKind(activate(V1))
[28] isNatList(n__nil) -> tt
[29] isNatList(n__cons(V1,V2)) ->
 U51(and(isNatKind(activate(V1)),n__isNatIListKind(activate(V2))),activate(V1),
  activate(V2))
[30] length(nil) -> 0
[31] length(cons(N,L)) ->
 U61(and(and(isNatList(activate(L)),n__isNatIListKind(activate(L))),
      n__and(isNat(N),n__isNatKind(N))),activate(L))
[32] zeros -> n__zeros
[33] 0 -> n__0
[34] length(X) -> n__length(X)
[35] s(X) -> n__s(X)
[36] cons(X1,X2) -> n__cons(X1,X2)
[37] isNatIListKind(X) -> n__isNatIListKind(X)
[38] nil -> n__nil
[39] and(X1,X2) -> n__and(X1,X2)
[40] isNatKind(X) -> n__isNatKind(X)
[41] activate(n__zeros) -> zeros
[42] activate(n__0) -> 0
[43] activate(n__length(X)) -> length(X)
[44] activate(n__s(X)) -> s(X)
[45] activate(n__cons(X1,X2)) -> cons(X1,X2)
[46] activate(n__isNatIListKind(X)) -> isNatIListKind(X)
[47] activate(n__nil) -> nil
[48] activate(n__and(X1,X2)) -> and(X1,X2)
[49] activate(n__isNatKind(X)) -> isNatKind(X)
[50] activate(X) -> X


Sub problem: 
guided: 

DP termination of:
<Marked_zeros , Marked_cons(0,n__zeros)>
<Marked_zeros , Marked_0>
<Marked_U11(tt,V1) , Marked_U12(isNatList(activate(V1)))>
<Marked_U11(tt,V1) , Marked_isNatList(activate(V1))>
<Marked_U11(tt,V1) , Marked_activate(V1)>
<Marked_U21(tt,V1) , Marked_U22(isNat(activate(V1)))>
<Marked_U21(tt,V1) , Marked_isNat(activate(V1))>
<Marked_U21(tt,V1) , Marked_activate(V1)>
<Marked_U31(tt,V) , Marked_U32(isNatList(activate(V)))>
<Marked_U31(tt,V) , Marked_isNatList(activate(V))>
<Marked_U31(tt,V) , Marked_activate(V)>
<Marked_U41(tt,V1,V2) , Marked_U42(isNat(activate(V1)),activate(V2))>
<Marked_U41(tt,V1,V2) , Marked_isNat(activate(V1))>
<Marked_U41(tt,V1,V2) , Marked_activate(V1)>
<Marked_U41(tt,V1,V2) , Marked_activate(V2)>
<Marked_U42(tt,V2) , Marked_U43(isNatIList(activate(V2)))>
<Marked_U42(tt,V2) , Marked_isNatIList(activate(V2))>
<Marked_U42(tt,V2) , Marked_activate(V2)>
<Marked_U51(tt,V1,V2) , Marked_U52(isNat(activate(V1)),activate(V2))>
<Marked_U51(tt,V1,V2) , Marked_isNat(activate(V1))>
<Marked_U51(tt,V1,V2) , Marked_activate(V1)>
<Marked_U51(tt,V1,V2) , Marked_activate(V2)>
<Marked_U52(tt,V2) , Marked_U53(isNatList(activate(V2)))>
<Marked_U52(tt,V2) , Marked_isNatList(activate(V2))>
<Marked_U52(tt,V2) , Marked_activate(V2)>
<Marked_U61(tt,L) , Marked_s(length(activate(L)))>
<Marked_U61(tt,L) , Marked_length(activate(L))>
<Marked_U61(tt,L) , Marked_activate(L)>
<Marked_and(tt,X) , Marked_activate(X)>
<Marked_isNat(n__length(V1)) , Marked_U11(isNatIListKind(activate(V1)),
                                activate(V1))>
<Marked_isNat(n__length(V1)) , Marked_isNatIListKind(activate(V1))>
<Marked_isNat(n__length(V1)) , Marked_activate(V1)>
<Marked_isNat(n__length(V1)) , Marked_activate(V1)>
<Marked_isNat(n__s(V1)) , Marked_U21(isNatKind(activate(V1)),activate(V1))>
<Marked_isNat(n__s(V1)) , Marked_isNatKind(activate(V1))>
<Marked_isNat(n__s(V1)) , Marked_activate(V1)>
<Marked_isNat(n__s(V1)) , Marked_activate(V1)>
<Marked_isNatIList(V) , Marked_U31(isNatIListKind(activate(V)),activate(V))>
<Marked_isNatIList(V) , Marked_isNatIListKind(activate(V))>
<Marked_isNatIList(V) , Marked_activate(V)>
<Marked_isNatIList(V) , Marked_activate(V)>
<Marked_isNatIList(n__cons(V1,V2)) , Marked_U41(and(isNatKind(activate(V1)),
                                                 n__isNatIListKind(activate(V2)))
                                                 ,activate(V1),activate(V2))>
<Marked_isNatIList(n__cons(V1,V2)) , Marked_and(isNatKind(activate(V1)),
                                      n__isNatIListKind(activate(V2)))>
<Marked_isNatIList(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))>
<Marked_isNatIList(n__cons(V1,V2)) , Marked_activate(V1)>
<Marked_isNatIList(n__cons(V1,V2)) , Marked_activate(V2)>
<Marked_isNatIList(n__cons(V1,V2)) , Marked_activate(V1)>
<Marked_isNatIList(n__cons(V1,V2)) , Marked_activate(V2)>
<Marked_isNatIListKind(n__cons(V1,V2)) , Marked_and(isNatKind(activate(V1)),
                                          n__isNatIListKind(activate(V2)))>
<Marked_isNatIListKind(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))>
<Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V1)>
<Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V2)>
<Marked_isNatKind(n__length(V1)) , Marked_isNatIListKind(activate(V1))>
<Marked_isNatKind(n__length(V1)) , Marked_activate(V1)>
<Marked_isNatKind(n__s(V1)) , Marked_isNatKind(activate(V1))>
<Marked_isNatKind(n__s(V1)) , Marked_activate(V1)>
<Marked_isNatList(n__cons(V1,V2)) , Marked_U51(and(isNatKind(activate(V1)),
                                                n__isNatIListKind(activate(V2))),
                                     activate(V1),activate(V2))>
<Marked_isNatList(n__cons(V1,V2)) , Marked_and(isNatKind(activate(V1)),
                                     n__isNatIListKind(activate(V2)))>
<Marked_isNatList(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))>
<Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)>
<Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)>
<Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)>
<Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)>
<Marked_length(nil) , Marked_0>
<Marked_length(cons(N,L)) , Marked_U61(and(and(isNatList(activate(L)),
                                            n__isNatIListKind(activate(L))),
                                        n__and(isNat(N),n__isNatKind(N))),
                             activate(L))>
<Marked_length(cons(N,L)) , Marked_and(and(isNatList(activate(L)),
                                        n__isNatIListKind(activate(L))),
                             n__and(isNat(N),n__isNatKind(N)))>
<Marked_length(cons(N,L)) , Marked_and(isNatList(activate(L)),
                             n__isNatIListKind(activate(L)))>
<Marked_length(cons(N,L)) , Marked_isNatList(activate(L))>
<Marked_length(cons(N,L)) , Marked_activate(L)>
<Marked_length(cons(N,L)) , Marked_activate(L)>
<Marked_length(cons(N,L)) , Marked_isNat(N)>
<Marked_length(cons(N,L)) , Marked_activate(L)>
<Marked_activate(n__zeros) , Marked_zeros>
<Marked_activate(n__0) , Marked_0>
<Marked_activate(n__length(X)) , Marked_length(X)>
<Marked_activate(n__s(X)) , Marked_s(X)>
<Marked_activate(n__cons(X1,X2)) , Marked_cons(X1,X2)>
<Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
<Marked_activate(n__nil) , Marked_nil>
<Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
<Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 2 components:

{  <Marked_isNatIList(n__cons(V1,V2)) , Marked_U41(and(isNatKind(activate(V1)),
                                                    n__isNatIListKind(
                                                     activate(V2))),
                                         activate(V1),activate(V2))> 
      --> <Marked_U41(tt,V1,V2) , Marked_U42(isNat(activate(V1)),activate(V2))>
  <Marked_U42(tt,V2) , Marked_isNatIList(activate(V2))> 
     --> <Marked_isNatIList(n__cons(V1,V2)) , Marked_U41(and(isNatKind(
                                                              activate(
                                                               V1)),
                                                          n__isNatIListKind(
                                                           activate(V2))),
                                               activate(V1),activate(V2))>
  <Marked_U41(tt,V1,V2) , Marked_U42(isNat(activate(V1)),activate(V2))> 
     --> <Marked_U42(tt,V2) , Marked_isNatIList(activate(V2))>
}

{  <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)> 
      --> <Marked_isNatKind(n__s(V1)) , Marked_activate(V1)>
  <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)> 
     --> <Marked_isNatKind(n__s(V1)) , Marked_isNatKind(activate(V1))>
  <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)> 
     --> <Marked_isNatKind(n__length(V1)) , Marked_activate(V1)>
  <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)> 
     --> <Marked_isNatKind(n__length(V1)) , Marked_isNatIListKind(activate(V1))>
  <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)> 
     --> <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V2)>
  <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)> 
     --> <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V1)>
  <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)> 
     --> <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))>
  <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)> 
     --> <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_and(isNatKind(
                                                              activate(
                                                               V1)),
                                                   n__isNatIListKind(
                                                    activate(V2)))>
  <Marked_activate(n__length(X)) , Marked_length(X)> 
     --> <Marked_length(cons(N,L)) , Marked_activate(L)>
  <Marked_activate(n__length(X)) , Marked_length(X)> 
     --> <Marked_length(cons(N,L)) , Marked_isNat(N)>
  <Marked_activate(n__length(X)) , Marked_length(X)> 
     --> <Marked_length(cons(N,L)) , Marked_activate(L)>
  <Marked_activate(n__length(X)) , Marked_length(X)> 
     --> <Marked_length(cons(N,L)) , Marked_activate(L)>
  <Marked_activate(n__length(X)) , Marked_length(X)> 
     --> <Marked_length(cons(N,L)) , Marked_isNatList(activate(L))>
  <Marked_activate(n__length(X)) , Marked_length(X)> 
     --> <Marked_length(cons(N,L)) , Marked_and(isNatList(activate(L)),
                                      n__isNatIListKind(activate(L)))>
  <Marked_activate(n__length(X)) , Marked_length(X)> 
     --> <Marked_length(cons(N,L)) , Marked_and(and(isNatList(activate(L)),
                                                 n__isNatIListKind(activate(L))),
                                      n__and(isNat(N),n__isNatKind(N)))>
  <Marked_activate(n__length(X)) , Marked_length(X)> 
     --> <Marked_length(cons(N,L)) , Marked_U61(and(and(isNatList(activate(L)),
                                                     n__isNatIListKind(
                                                      activate(L))),
                                                 n__and(isNat(N),
                                                  n__isNatKind(N))),
                                      activate(L))>
  <Marked_length(cons(N,L)) , Marked_activate(L)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_length(cons(N,L)) , Marked_activate(L)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_length(cons(N,L)) , Marked_activate(L)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_length(cons(N,L)) , Marked_activate(L)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_length(cons(N,L)) , Marked_isNat(N)> 
     --> <Marked_isNat(n__s(V1)) , Marked_activate(V1)>
  <Marked_length(cons(N,L)) , Marked_isNat(N)> 
     --> <Marked_isNat(n__s(V1)) , Marked_activate(V1)>
  <Marked_length(cons(N,L)) , Marked_isNat(N)> 
     --> <Marked_isNat(n__s(V1)) , Marked_isNatKind(activate(V1))>
  <Marked_length(cons(N,L)) , Marked_isNat(N)> 
     --> <Marked_isNat(n__s(V1)) , Marked_U21(isNatKind(activate(V1)),
                                    activate(V1))>
  <Marked_length(cons(N,L)) , Marked_isNat(N)> 
     --> <Marked_isNat(n__length(V1)) , Marked_activate(V1)>
  <Marked_length(cons(N,L)) , Marked_isNat(N)> 
     --> <Marked_isNat(n__length(V1)) , Marked_activate(V1)>
  <Marked_length(cons(N,L)) , Marked_isNat(N)> 
     --> <Marked_isNat(n__length(V1)) , Marked_isNatIListKind(activate(V1))>
  <Marked_length(cons(N,L)) , Marked_isNat(N)> 
     --> <Marked_isNat(n__length(V1)) , Marked_U11(isNatIListKind(activate(V1)),
                                         activate(V1))>
  <Marked_length(cons(N,L)) , Marked_activate(L)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_length(cons(N,L)) , Marked_activate(L)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_length(cons(N,L)) , Marked_activate(L)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_length(cons(N,L)) , Marked_activate(L)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_length(cons(N,L)) , Marked_activate(L)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_length(cons(N,L)) , Marked_activate(L)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_length(cons(N,L)) , Marked_activate(L)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_length(cons(N,L)) , Marked_activate(L)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_length(cons(N,L)) , Marked_isNatList(activate(L))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)>
  <Marked_length(cons(N,L)) , Marked_isNatList(activate(L))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)>
  <Marked_length(cons(N,L)) , Marked_isNatList(activate(L))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)>
  <Marked_length(cons(N,L)) , Marked_isNatList(activate(L))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)>
  <Marked_length(cons(N,L)) , Marked_isNatList(activate(L))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))>
  <Marked_length(cons(N,L)) , Marked_isNatList(activate(L))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_and(isNatKind(activate(V1)),
                                              n__isNatIListKind(activate(V2)))>
  <Marked_length(cons(N,L)) , Marked_isNatList(activate(L))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_U51(and(isNatKind(
                                                             activate(
                                                              V1)),
                                                         n__isNatIListKind(
                                                          activate(V2))),
                                              activate(V1),activate(V2))>
  <Marked_length(cons(N,L)) , Marked_and(isNatList(activate(L)),
                               n__isNatIListKind(activate(L)))> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_length(cons(N,L)) , Marked_and(and(isNatList(activate(L)),
                                          n__isNatIListKind(activate(L))),
                               n__and(isNat(N),n__isNatKind(N)))> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_length(cons(N,L)) , Marked_U61(and(and(isNatList(activate(L)),
                                              n__isNatIListKind(activate(L))),
                                          n__and(isNat(N),n__isNatKind(N))),
                               activate(L))> 
     --> <Marked_U61(tt,L) , Marked_activate(L)>
  <Marked_length(cons(N,L)) , Marked_U61(and(and(isNatList(activate(L)),
                                              n__isNatIListKind(activate(L))),
                                          n__and(isNat(N),n__isNatKind(N))),
                               activate(L))> 
     --> <Marked_U61(tt,L) , Marked_length(activate(L))>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__s(V1)) , Marked_activate(V1)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__s(V1)) , Marked_isNatKind(activate(V1))>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__length(V1)) , Marked_activate(V1)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__length(V1)) , Marked_isNatIListKind(activate(V1))>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_and(isNatKind(activate(V1)),
                                       n__isNatIListKind(activate(V2)))> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_U51(and(isNatKind(activate(V1)),
                                                  n__isNatIListKind(activate(
                                                                    V2))),
                                       activate(V1),activate(V2))> 
     --> <Marked_U51(tt,V1,V2) , Marked_activate(V2)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_U51(and(isNatKind(activate(V1)),
                                                  n__isNatIListKind(activate(
                                                                    V2))),
                                       activate(V1),activate(V2))> 
     --> <Marked_U51(tt,V1,V2) , Marked_activate(V1)>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_U51(and(isNatKind(activate(V1)),
                                                  n__isNatIListKind(activate(
                                                                    V2))),
                                       activate(V1),activate(V2))> 
     --> <Marked_U51(tt,V1,V2) , Marked_isNat(activate(V1))>
  <Marked_isNatList(n__cons(V1,V2)) , Marked_U51(and(isNatKind(activate(V1)),
                                                  n__isNatIListKind(activate(
                                                                    V2))),
                                       activate(V1),activate(V2))> 
     --> <Marked_U51(tt,V1,V2) , Marked_U52(isNat(activate(V1)),activate(V2))>
  <Marked_isNatKind(n__s(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_isNatKind(n__s(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_isNatKind(n__s(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_isNatKind(n__s(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_isNatKind(n__s(V1)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__s(V1)) , Marked_activate(V1)>
  <Marked_isNatKind(n__s(V1)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__s(V1)) , Marked_isNatKind(activate(V1))>
  <Marked_isNatKind(n__s(V1)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__length(V1)) , Marked_activate(V1)>
  <Marked_isNatKind(n__s(V1)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__length(V1)) , Marked_isNatIListKind(activate(V1))>
  <Marked_isNatKind(n__length(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_isNatKind(n__length(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_isNatKind(n__length(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_isNatKind(n__length(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_isNatKind(n__length(V1)) , Marked_isNatIListKind(activate(V1))> 
     --> <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V2)>
  <Marked_isNatKind(n__length(V1)) , Marked_isNatIListKind(activate(V1))> 
     --> <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V1)>
  <Marked_isNatKind(n__length(V1)) , Marked_isNatIListKind(activate(V1))> 
     --> <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))>
  <Marked_isNatKind(n__length(V1)) , Marked_isNatIListKind(activate(V1))> 
     --> <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_and(isNatKind(
                                                              activate(
                                                               V1)),
                                                   n__isNatIListKind(
                                                    activate(V2)))>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__s(V1)) , Marked_activate(V1)>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__s(V1)) , Marked_isNatKind(activate(V1))>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__length(V1)) , Marked_activate(V1)>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__length(V1)) , Marked_isNatIListKind(activate(V1))>
  <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_and(isNatKind(activate(V1)),
                                            n__isNatIListKind(activate(V2)))> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_isNat(n__s(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_isNat(n__s(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_isNat(n__s(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_isNat(n__s(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_isNat(n__s(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_isNat(n__s(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_isNat(n__s(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_isNat(n__s(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_isNat(n__s(V1)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__s(V1)) , Marked_activate(V1)>
  <Marked_isNat(n__s(V1)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__s(V1)) , Marked_isNatKind(activate(V1))>
  <Marked_isNat(n__s(V1)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__length(V1)) , Marked_activate(V1)>
  <Marked_isNat(n__s(V1)) , Marked_isNatKind(activate(V1))> 
     --> <Marked_isNatKind(n__length(V1)) , Marked_isNatIListKind(activate(V1))>
  <Marked_isNat(n__s(V1)) , Marked_U21(isNatKind(activate(V1)),activate(V1))> 
     --> <Marked_U21(tt,V1) , Marked_activate(V1)>
  <Marked_isNat(n__s(V1)) , Marked_U21(isNatKind(activate(V1)),activate(V1))> 
     --> <Marked_U21(tt,V1) , Marked_isNat(activate(V1))>
  <Marked_isNat(n__length(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_isNat(n__length(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_isNat(n__length(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_isNat(n__length(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_isNat(n__length(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_isNat(n__length(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_isNat(n__length(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_isNat(n__length(V1)) , Marked_activate(V1)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_isNat(n__length(V1)) , Marked_isNatIListKind(activate(V1))> 
     --> <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V2)>
  <Marked_isNat(n__length(V1)) , Marked_isNatIListKind(activate(V1))> 
     --> <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_activate(V1)>
  <Marked_isNat(n__length(V1)) , Marked_isNatIListKind(activate(V1))> 
     --> <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))>
  <Marked_isNat(n__length(V1)) , Marked_isNatIListKind(activate(V1))> 
     --> <Marked_isNatIListKind(n__cons(V1,V2)) , Marked_and(isNatKind(
                                                              activate(
                                                               V1)),
                                                   n__isNatIListKind(
                                                    activate(V2)))>
  <Marked_isNat(n__length(V1)) , Marked_U11(isNatIListKind(activate(V1)),
                                  activate(V1))> 
     --> <Marked_U11(tt,V1) , Marked_activate(V1)>
  <Marked_isNat(n__length(V1)) , Marked_U11(isNatIListKind(activate(V1)),
                                  activate(V1))> 
     --> <Marked_U11(tt,V1) , Marked_isNatList(activate(V1))>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_U61(tt,L) , Marked_activate(L)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_U61(tt,L) , Marked_activate(L)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_U61(tt,L) , Marked_activate(L)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_U61(tt,L) , Marked_activate(L)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_U61(tt,L) , Marked_length(activate(L))> 
     --> <Marked_length(cons(N,L)) , Marked_activate(L)>
  <Marked_U61(tt,L) , Marked_length(activate(L))> 
     --> <Marked_length(cons(N,L)) , Marked_isNat(N)>
  <Marked_U61(tt,L) , Marked_length(activate(L))> 
     --> <Marked_length(cons(N,L)) , Marked_activate(L)>
  <Marked_U61(tt,L) , Marked_length(activate(L))> 
     --> <Marked_length(cons(N,L)) , Marked_activate(L)>
  <Marked_U61(tt,L) , Marked_length(activate(L))> 
     --> <Marked_length(cons(N,L)) , Marked_isNatList(activate(L))>
  <Marked_U61(tt,L) , Marked_length(activate(L))> 
     --> <Marked_length(cons(N,L)) , Marked_and(isNatList(activate(L)),
                                      n__isNatIListKind(activate(L)))>
  <Marked_U61(tt,L) , Marked_length(activate(L))> 
     --> <Marked_length(cons(N,L)) , Marked_and(and(isNatList(activate(L)),
                                                 n__isNatIListKind(activate(L))),
                                      n__and(isNat(N),n__isNatKind(N)))>
  <Marked_U61(tt,L) , Marked_length(activate(L))> 
     --> <Marked_length(cons(N,L)) , Marked_U61(and(and(isNatList(activate(L)),
                                                     n__isNatIListKind(
                                                      activate(L))),
                                                 n__and(isNat(N),
                                                  n__isNatKind(N))),
                                      activate(L))>
  <Marked_U52(tt,V2) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_U52(tt,V2) , Marked_activate(V2)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_U52(tt,V2) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_U52(tt,V2) , Marked_activate(V2)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_U52(tt,V2) , Marked_isNatList(activate(V2))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)>
  <Marked_U52(tt,V2) , Marked_isNatList(activate(V2))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)>
  <Marked_U52(tt,V2) , Marked_isNatList(activate(V2))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)>
  <Marked_U52(tt,V2) , Marked_isNatList(activate(V2))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)>
  <Marked_U52(tt,V2) , Marked_isNatList(activate(V2))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))>
  <Marked_U52(tt,V2) , Marked_isNatList(activate(V2))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_and(isNatKind(activate(V1)),
                                              n__isNatIListKind(activate(V2)))>
  <Marked_U52(tt,V2) , Marked_isNatList(activate(V2))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_U51(and(isNatKind(
                                                             activate(
                                                              V1)),
                                                         n__isNatIListKind(
                                                          activate(V2))),
                                              activate(V1),activate(V2))>
  <Marked_U51(tt,V1,V2) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_U51(tt,V1,V2) , Marked_activate(V2)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_U51(tt,V1,V2) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_U51(tt,V1,V2) , Marked_activate(V2)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_U51(tt,V1,V2) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_U51(tt,V1,V2) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_U51(tt,V1,V2) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_U51(tt,V1,V2) , Marked_activate(V1)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_U51(tt,V1,V2) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__s(V1)) , Marked_activate(V1)>
  <Marked_U51(tt,V1,V2) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__s(V1)) , Marked_activate(V1)>
  <Marked_U51(tt,V1,V2) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__s(V1)) , Marked_isNatKind(activate(V1))>
  <Marked_U51(tt,V1,V2) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__s(V1)) , Marked_U21(isNatKind(activate(V1)),
                                    activate(V1))>
  <Marked_U51(tt,V1,V2) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__length(V1)) , Marked_activate(V1)>
  <Marked_U51(tt,V1,V2) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__length(V1)) , Marked_activate(V1)>
  <Marked_U51(tt,V1,V2) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__length(V1)) , Marked_isNatIListKind(activate(V1))>
  <Marked_U51(tt,V1,V2) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__length(V1)) , Marked_U11(isNatIListKind(activate(V1)),
                                         activate(V1))>
  <Marked_U51(tt,V1,V2) , Marked_U52(isNat(activate(V1)),activate(V2))> 
     --> <Marked_U52(tt,V2) , Marked_activate(V2)>
  <Marked_U51(tt,V1,V2) , Marked_U52(isNat(activate(V1)),activate(V2))> 
     --> <Marked_U52(tt,V2) , Marked_isNatList(activate(V2))>
  <Marked_U21(tt,V1) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_U21(tt,V1) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_U21(tt,V1) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_U21(tt,V1) , Marked_activate(V1)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_U21(tt,V1) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__s(V1)) , Marked_activate(V1)>
  <Marked_U21(tt,V1) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__s(V1)) , Marked_activate(V1)>
  <Marked_U21(tt,V1) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__s(V1)) , Marked_isNatKind(activate(V1))>
  <Marked_U21(tt,V1) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__s(V1)) , Marked_U21(isNatKind(activate(V1)),
                                    activate(V1))>
  <Marked_U21(tt,V1) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__length(V1)) , Marked_activate(V1)>
  <Marked_U21(tt,V1) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__length(V1)) , Marked_activate(V1)>
  <Marked_U21(tt,V1) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__length(V1)) , Marked_isNatIListKind(activate(V1))>
  <Marked_U21(tt,V1) , Marked_isNat(activate(V1))> 
     --> <Marked_isNat(n__length(V1)) , Marked_U11(isNatIListKind(activate(V1)),
                                         activate(V1))>
  <Marked_U11(tt,V1) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatKind(X)) , Marked_isNatKind(X)>
  <Marked_U11(tt,V1) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(X1,X2)>
  <Marked_U11(tt,V1) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNatIListKind(X)) , Marked_isNatIListKind(X)>
  <Marked_U11(tt,V1) , Marked_activate(V1)> 
     --> <Marked_activate(n__length(X)) , Marked_length(X)>
  <Marked_U11(tt,V1) , Marked_isNatList(activate(V1))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)>
  <Marked_U11(tt,V1) , Marked_isNatList(activate(V1))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)>
  <Marked_U11(tt,V1) , Marked_isNatList(activate(V1))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V2)>
  <Marked_U11(tt,V1) , Marked_isNatList(activate(V1))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_activate(V1)>
  <Marked_U11(tt,V1) , Marked_isNatList(activate(V1))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_isNatKind(activate(V1))>
  <Marked_U11(tt,V1) , Marked_isNatList(activate(V1))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_and(isNatKind(activate(V1)),
                                              n__isNatIListKind(activate(V2)))>
  <Marked_U11(tt,V1) , Marked_isNatList(activate(V1))> 
     --> <Marked_isNatList(n__cons(V1,V2)) , Marked_U51(and(isNatKind(
                                                             activate(
                                                              V1)),
                                                         n__isNatIListKind(
                                                          activate(V2))),
                                              activate(V1),activate(V2))>
}
APPLY CRITERIA (Subterm criterion)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  cons(X1,X2) >= n__cons(X1,X2) ;
  0 >= n__0 ;
  zeros >= cons(0,n__zeros) ;
  zeros >= n__zeros ;
  U12(tt) >= tt ;
  isNatList(n__cons(V1,V2)) >= U51(and(isNatKind(activate(V1)),
                                    n__isNatIListKind(activate(V2))),
                                activate(V1),activate(V2)) ;
  isNatList(n__nil) >= tt ;
  activate(n__zeros) >= zeros ;
  activate(n__0) >= 0 ;
  activate(n__length(X)) >= length(X) ;
  activate(n__s(X)) >= s(X) ;
  activate(n__isNatIListKind(X)) >= isNatIListKind(X) ;
  activate(n__cons(X1,X2)) >= cons(X1,X2) ;
  activate(n__nil) >= nil ;
  activate(n__and(X1,X2)) >= and(X1,X2) ;
  activate(n__isNatKind(X)) >= isNatKind(X) ;
  activate(X) >= X ;
  U11(tt,V1) >= U12(isNatList(activate(V1))) ;
  U22(tt) >= tt ;
  isNat(n__0) >= tt ;
  isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)),activate(V1)) ;
  isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) ;
  U21(tt,V1) >= U22(isNat(activate(V1))) ;
  U32(tt) >= tt ;
  U31(tt,V) >= U32(isNatList(activate(V))) ;
  U42(tt,V2) >= U43(isNatIList(activate(V2))) ;
  U41(tt,V1,V2) >= U42(isNat(activate(V1)),activate(V2)) ;
  U43(tt) >= tt ;
  isNatIList(n__zeros) >= tt ;
  isNatIList(n__cons(V1,V2)) >= U41(and(isNatKind(activate(V1)),
                                     n__isNatIListKind(activate(V2))),
                                 activate(V1),activate(V2)) ;
  isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) ;
  U52(tt,V2) >= U53(isNatList(activate(V2))) ;
  U51(tt,V1,V2) >= U52(isNat(activate(V1)),activate(V2)) ;
  U53(tt) >= tt ;
  s(X) >= n__s(X) ;
  length(cons(N,L)) >= U61(and(and(isNatList(activate(L)),
                                n__isNatIListKind(activate(L))),
                            n__and(isNat(N),n__isNatKind(N))),activate(L)) ;
  length(nil) >= 0 ;
  length(X) >= n__length(X) ;
  U61(tt,L) >= s(length(activate(L))) ;
  and(tt,X) >= activate(X) ;
  and(X1,X2) >= n__and(X1,X2) ;
  isNatIListKind(n__zeros) >= tt ;
  isNatIListKind(n__cons(V1,V2)) >= and(isNatKind(activate(V1)),
                                     n__isNatIListKind(activate(V2))) ;
  isNatIListKind(n__nil) >= tt ;
  isNatIListKind(X) >= n__isNatIListKind(X) ;
  isNatKind(n__0) >= tt ;
  isNatKind(n__length(V1)) >= isNatIListKind(activate(V1)) ;
  isNatKind(n__s(V1)) >= isNatKind(activate(V1)) ;
  isNatKind(X) >= n__isNatKind(X) ;
  nil >= n__nil ;
  Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(and(isNatKind(activate(V1)),
                                                   n__isNatIListKind(
                                                    activate(V2))),
                                        activate(V1),activate(V2)) ;
  Marked_U41(tt,V1,V2) >= Marked_U42(isNat(activate(V1)),activate(V2)) ;
  Marked_U42(tt,V2) >= Marked_isNatIList(activate(V2)) ;
 }
 + Disjunctions:{ 
{
  Marked_isNatIList(n__cons(V1,V2)) > Marked_U41(and(isNatKind(activate(V1)),
                                                  n__isNatIListKind(activate(
                                                                    V2))),
                                       activate(V1),activate(V2)) ;
 }
{
  Marked_U41(tt,V1,V2) > Marked_U42(isNat(activate(V1)),activate(V2)) ;
 }
{
  Marked_U42(tt,V2) > Marked_isNatIList(activate(V2)) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
Entering rpo_solver
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
Time out for these parameters.
=== TIMER virtual : 15.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 15.000000 ===
=== STOPING TIMER real ===
Sat timeout reached
=== STOPING TIMER virtual ===
Time out for these parameters.
=== TIMER virtual : 50.000000 ===
trying sub matrices of size: 1
Matrix interpretation constraints generated.
Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. 
Termination constraints generated.
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 50.000000 ===
=== STOPING TIMER real ===
Sat timeout reached
=== STOPING TIMER virtual ===
No solution found for these parameters.
No solution found for these constraints.
APPLY CRITERIA (Simple graph)
Found the following constraints:
{
  cons(X1,X2) >= n__cons(X1,X2) ;
  0 >= n__0 ;
  zeros >= cons(0,n__zeros) ;
  zeros >= n__zeros ;
  U12(tt) >= tt ;
  isNatList(n__cons(V1,V2)) >= U51(and(isNatKind(activate(V1)),
                                    n__isNatIListKind(activate(V2))),
                                activate(V1),activate(V2)) ;
  isNatList(n__nil) >= tt ;
  activate(n__zeros) >= zeros ;
  activate(n__0) >= 0 ;
  activate(n__length(X)) >= length(X) ;
  activate(n__s(X)) >= s(X) ;
  activate(n__isNatIListKind(X)) >= isNatIListKind(X) ;
  activate(n__cons(X1,X2)) >= cons(X1,X2) ;
  activate(n__nil) >= nil ;
  activate(n__and(X1,X2)) >= and(X1,X2) ;
  activate(n__isNatKind(X)) >= isNatKind(X) ;
  activate(X) >= X ;
  U11(tt,V1) >= U12(isNatList(activate(V1))) ;
  U22(tt) >= tt ;
  isNat(n__0) >= tt ;
  isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)),activate(V1)) ;
  isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) ;
  U21(tt,V1) >= U22(isNat(activate(V1))) ;
  U32(tt) >= tt ;
  U31(tt,V) >= U32(isNatList(activate(V))) ;
  U42(tt,V2) >= U43(isNatIList(activate(V2))) ;
  U41(tt,V1,V2) >= U42(isNat(activate(V1)),activate(V2)) ;
  U43(tt) >= tt ;
  isNatIList(n__zeros) >= tt ;
  isNatIList(n__cons(V1,V2)) >= U41(and(isNatKind(activate(V1)),
                                     n__isNatIListKind(activate(V2))),
                                 activate(V1),activate(V2)) ;
  isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) ;
  U52(tt,V2) >= U53(isNatList(activate(V2))) ;
  U51(tt,V1,V2) >= U52(isNat(activate(V1)),activate(V2)) ;
  U53(tt) >= tt ;
  s(X) >= n__s(X) ;
  length(cons(N,L)) >= U61(and(and(isNatList(activate(L)),
                                n__isNatIListKind(activate(L))),
                            n__and(isNat(N),n__isNatKind(N))),activate(L)) ;
  length(nil) >= 0 ;
  length(X) >= n__length(X) ;
  U61(tt,L) >= s(length(activate(L))) ;
  and(tt,X) >= activate(X) ;
  and(X1,X2) >= n__and(X1,X2) ;
  isNatIListKind(n__zeros) >= tt ;
  isNatIListKind(n__cons(V1,V2)) >= and(isNatKind(activate(V1)),
                                     n__isNatIListKind(activate(V2))) ;
  isNatIListKind(n__nil) >= tt ;
  isNatIListKind(X) >= n__isNatIListKind(X) ;
  isNatKind(n__0) >= tt ;
  isNatKind(n__length(V1)) >= isNatIListKind(activate(V1)) ;
  isNatKind(n__s(V1)) >= isNatKind(activate(V1)) ;
  isNatKind(X) >= n__isNatKind(X) ;
  nil >= n__nil ;
  Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(and(isNatKind(activate(V1)),
                                                   n__isNatIListKind(
                                                    activate(V2))),
                                        activate(V1),activate(V2)) ;
  Marked_U41(tt,V1,V2) >= Marked_U42(isNat(activate(V1)),activate(V2)) ;
  Marked_U42(tt,V2) > Marked_isNatIList(activate(V2)) ;
 }

APPLY CRITERIA (SOLVE_ORD)
Trying to solve the following constraints:
{
  cons(X1,X2) >= n__cons(X1,X2) ;
  0 >= n__0 ;
  zeros >= cons(0,n__zeros) ;
  zeros >= n__zeros ;
  U12(tt) >= tt ;
  isNatList(n__cons(V1,V2)) >= U51(and(isNatKind(activate(V1)),
                                    n__isNatIListKind(activate(V2))),
                                activate(V1),activate(V2)) ;
  isNatList(n__nil) >= tt ;
  activate(n__zeros) >= zeros ;
  activate(n__0) >= 0 ;
  activate(n__length(X)) >= length(X) ;
  activate(n__s(X)) >= s(X) ;
  activate(n__isNatIListKind(X)) >= isNatIListKind(X) ;
  activate(n__cons(X1,X2)) >= cons(X1,X2) ;
  activate(n__nil) >= nil ;
  activate(n__and(X1,X2)) >= and(X1,X2) ;
  activate(n__isNatKind(X)) >= isNatKind(X) ;
  activate(X) >= X ;
  U11(tt,V1) >= U12(isNatList(activate(V1))) ;
  U22(tt) >= tt ;
  isNat(n__0) >= tt ;
  isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)),activate(V1)) ;
  isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) ;
  U21(tt,V1) >= U22(isNat(activate(V1))) ;
  U32(tt) >= tt ;
  U31(tt,V) >= U32(isNatList(activate(V))) ;
  U42(tt,V2) >= U43(isNatIList(activate(V2))) ;
  U41(tt,V1,V2) >= U42(isNat(activate(V1)),activate(V2)) ;
  U43(tt) >= tt ;
  isNatIList(n__zeros) >= tt ;
  isNatIList(n__cons(V1,V2)) >= U41(and(isNatKind(activate(V1)),
                                     n__isNatIListKind(activate(V2))),
                                 activate(V1),activate(V2)) ;
  isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) ;
  U52(tt,V2) >= U53(isNatList(activate(V2))) ;
  U51(tt,V1,V2) >= U52(isNat(activate(V1)),activate(V2)) ;
  U53(tt) >= tt ;
  s(X) >= n__s(X) ;
  length(cons(N,L)) >= U61(and(and(isNatList(activate(L)),
                                n__isNatIListKind(activate(L))),
                            n__and(isNat(N),n__isNatKind(N))),activate(L)) ;
  length(nil) >= 0 ;
  length(X) >= n__length(X) ;
  U61(tt,L) >= s(length(activate(L))) ;
  and(tt,X) >= activate(X) ;
  and(X1,X2) >= n__and(X1,X2) ;
  isNatIListKind(n__zeros) >= tt ;
  isNatIListKind(n__cons(V1,V2)) >= and(isNatKind(activate(V1)),
                                     n__isNatIListKind(activate(V2))) ;
  isNatIListKind(n__nil) >= tt ;
  isNatIListKind(X) >= n__isNatIListKind(X) ;
  isNatKind(n__0) >= tt ;
  isNatKind(n__length(V1)) >= isNatIListKind(activate(V1)) ;
  isNatKind(n__s(V1)) >= isNatKind(activate(V1)) ;
  isNatKind(X) >= n__isNatKind(X) ;
  nil >= n__nil ;
  Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(and(isNatKind(activate(V1)),
                                                   n__isNatIListKind(
                                                    activate(V2))),
                                        activate(V1),activate(V2)) ;
  Marked_U41(tt,V1,V2) >= Marked_U42(isNat(activate(V1)),activate(V2)) ;
  Marked_U42(tt,V2) > Marked_isNatIList(activate(V2)) ;
 }
 + Disjunctions:{ 
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
Entering rpo_solver
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
Time out for these parameters.
=== TIMER virtual : 15.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 15.000000 ===
=== STOPING TIMER real ===
Sat timeout reached
=== STOPING TIMER virtual ===
Time out for these parameters.
=== TIMER virtual : 50.000000 ===
trying sub matrices of size: 1
Matrix interpretation constraints generated.
Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. 
Termination constraints generated.
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 50.000000 ===
=== STOPING TIMER real ===
Sat timeout reached
=== STOPING TIMER virtual ===
No solution found for these parameters.
No solution found for these constraints.
APPLY CRITERIA (ID_CRIT)
NOT SOLVED
No proof found
Cime worked for 204.416190 seconds (real time)
Cime Exit Status: 0