Input TRS:
    1: active(U11(tt(),V1,V2)) -> mark(U12(isNat(V1),V2))
    2: active(U12(tt(),V2)) -> mark(U13(isNat(V2)))
    3: active(U13(tt())) -> mark(tt())
    4: active(U21(tt(),V1)) -> mark(U22(isNat(V1)))
    5: active(U22(tt())) -> mark(tt())
    6: active(U31(tt(),V1,V2)) -> mark(U32(isNat(V1),V2))
    7: active(U32(tt(),V2)) -> mark(U33(isNat(V2)))
    8: active(U33(tt())) -> mark(tt())
    9: active(U41(tt(),N)) -> mark(N)
    10: active(U51(tt(),M,N)) -> mark(s(plus(N,M)))
    11: active(U61(tt())) -> mark(0())
    12: active(U71(tt(),M,N)) -> mark(plus(x(N,M),N))
    13: active(and(tt(),X)) -> mark(X)
    14: active(isNat(0())) -> mark(tt())
    15: active(isNat(plus(V1,V2))) -> mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
    16: active(isNat(s(V1))) -> mark(U21(isNatKind(V1),V1))
    17: active(isNat(x(V1,V2))) -> mark(U31(and(isNatKind(V1),isNatKind(V2)),V1,V2))
    18: active(isNatKind(0())) -> mark(tt())
    19: active(isNatKind(plus(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
    20: active(isNatKind(s(V1))) -> mark(isNatKind(V1))
    21: active(isNatKind(x(V1,V2))) -> mark(and(isNatKind(V1),isNatKind(V2)))
    22: active(plus(N,0())) -> mark(U41(and(isNat(N),isNatKind(N)),N))
    23: active(plus(N,s(M))) -> mark(U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
    24: active(x(N,0())) -> mark(U61(and(isNat(N),isNatKind(N))))
    25: active(x(N,s(M))) -> mark(U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
    26: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3))
    27: mark(tt()) -> active(tt())
    28: mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
    29: mark(isNat(X)) -> active(isNat(X))
    30: mark(U13(X)) -> active(U13(mark(X)))
    31: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
    32: mark(U22(X)) -> active(U22(mark(X)))
    33: mark(U31(X1,X2,X3)) -> active(U31(mark(X1),X2,X3))
    34: mark(U32(X1,X2)) -> active(U32(mark(X1),X2))
    35: mark(U33(X)) -> active(U33(mark(X)))
    36: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
    37: mark(U51(X1,X2,X3)) -> active(U51(mark(X1),X2,X3))
    38: mark(s(X)) -> active(s(mark(X)))
    39: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
    40: mark(U61(X)) -> active(U61(mark(X)))
    41: mark(0()) -> active(0())
    42: mark(U71(X1,X2,X3)) -> active(U71(mark(X1),X2,X3))
    43: mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
    44: mark(and(X1,X2)) -> active(and(mark(X1),X2))
    45: mark(isNatKind(X)) -> active(isNatKind(X))
    46: U11(mark(X1),X2,X3) -> U11(X1,X2,X3)
    47: U11(X1,mark(X2),X3) -> U11(X1,X2,X3)
    48: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3)
    49: U11(active(X1),X2,X3) -> U11(X1,X2,X3)
    50: U11(X1,active(X2),X3) -> U11(X1,X2,X3)
    51: U11(X1,X2,active(X3)) -> U11(X1,X2,X3)
    52: U12(mark(X1),X2) -> U12(X1,X2)
    53: U12(X1,mark(X2)) -> U12(X1,X2)
    54: U12(active(X1),X2) -> U12(X1,X2)
    55: U12(X1,active(X2)) -> U12(X1,X2)
    56: isNat(mark(X)) -> isNat(X)
    57: isNat(active(X)) -> isNat(X)
    58: U13(mark(X)) -> U13(X)
    59: U13(active(X)) -> U13(X)
    60: U21(mark(X1),X2) -> U21(X1,X2)
    61: U21(X1,mark(X2)) -> U21(X1,X2)
    62: U21(active(X1),X2) -> U21(X1,X2)
    63: U21(X1,active(X2)) -> U21(X1,X2)
    64: U22(mark(X)) -> U22(X)
    65: U22(active(X)) -> U22(X)
    66: U31(mark(X1),X2,X3) -> U31(X1,X2,X3)
    67: U31(X1,mark(X2),X3) -> U31(X1,X2,X3)
    68: U31(X1,X2,mark(X3)) -> U31(X1,X2,X3)
    69: U31(active(X1),X2,X3) -> U31(X1,X2,X3)
    70: U31(X1,active(X2),X3) -> U31(X1,X2,X3)
    71: U31(X1,X2,active(X3)) -> U31(X1,X2,X3)
    72: U32(mark(X1),X2) -> U32(X1,X2)
    73: U32(X1,mark(X2)) -> U32(X1,X2)
    74: U32(active(X1),X2) -> U32(X1,X2)
    75: U32(X1,active(X2)) -> U32(X1,X2)
    76: U33(mark(X)) -> U33(X)
    77: U33(active(X)) -> U33(X)
    78: U41(mark(X1),X2) -> U41(X1,X2)
    79: U41(X1,mark(X2)) -> U41(X1,X2)
    80: U41(active(X1),X2) -> U41(X1,X2)
    81: U41(X1,active(X2)) -> U41(X1,X2)
    82: U51(mark(X1),X2,X3) -> U51(X1,X2,X3)
    83: U51(X1,mark(X2),X3) -> U51(X1,X2,X3)
    84: U51(X1,X2,mark(X3)) -> U51(X1,X2,X3)
    85: U51(active(X1),X2,X3) -> U51(X1,X2,X3)
    86: U51(X1,active(X2),X3) -> U51(X1,X2,X3)
    87: U51(X1,X2,active(X3)) -> U51(X1,X2,X3)
    88: s(mark(X)) -> s(X)
    89: s(active(X)) -> s(X)
    90: plus(mark(X1),X2) -> plus(X1,X2)
    91: plus(X1,mark(X2)) -> plus(X1,X2)
    92: plus(active(X1),X2) -> plus(X1,X2)
    93: plus(X1,active(X2)) -> plus(X1,X2)
    94: U61(mark(X)) -> U61(X)
    95: U61(active(X)) -> U61(X)
    96: U71(mark(X1),X2,X3) -> U71(X1,X2,X3)
    97: U71(X1,mark(X2),X3) -> U71(X1,X2,X3)
    98: U71(X1,X2,mark(X3)) -> U71(X1,X2,X3)
    99: U71(active(X1),X2,X3) -> U71(X1,X2,X3)
    100: U71(X1,active(X2),X3) -> U71(X1,X2,X3)
    101: U71(X1,X2,active(X3)) -> U71(X1,X2,X3)
    102: x(mark(X1),X2) -> x(X1,X2)
    103: x(X1,mark(X2)) -> x(X1,X2)
    104: x(active(X1),X2) -> x(X1,X2)
    105: x(X1,active(X2)) -> x(X1,X2)
    106: and(mark(X1),X2) -> and(X1,X2)
    107: and(X1,mark(X2)) -> and(X1,X2)
    108: and(active(X1),X2) -> and(X1,X2)
    109: and(X1,active(X2)) -> and(X1,X2)
    110: isNatKind(mark(X)) -> isNatKind(X)
    111: isNatKind(active(X)) -> isNatKind(X)
Number of strict rules: 111
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(U12(tt(),V2)) -> #mark(U13(isNat(V2)))
   #2: #active(U12(tt(),V2)) -> #U13(isNat(V2))
   #3: #active(U12(tt(),V2)) -> #isNat(V2)
   #4: #U51(X1,active(X2),X3) -> #U51(X1,X2,X3)
   #5: #mark(x(X1,X2)) -> #active(x(mark(X1),mark(X2)))
   #6: #mark(x(X1,X2)) -> #x(mark(X1),mark(X2))
   #7: #mark(x(X1,X2)) -> #mark(X1)
   #8: #mark(x(X1,X2)) -> #mark(X2)
   #9: #mark(isNat(X)) -> #active(isNat(X))
   #10: #mark(U33(X)) -> #active(U33(mark(X)))
   #11: #mark(U33(X)) -> #U33(mark(X))
   #12: #mark(U33(X)) -> #mark(X)
   #13: #U51(X1,mark(X2),X3) -> #U51(X1,X2,X3)
   #14: #U31(mark(X1),X2,X3) -> #U31(X1,X2,X3)
   #15: #U11(mark(X1),X2,X3) -> #U11(X1,X2,X3)
   #16: #mark(U71(X1,X2,X3)) -> #active(U71(mark(X1),X2,X3))
   #17: #mark(U71(X1,X2,X3)) -> #U71(mark(X1),X2,X3)
   #18: #mark(U71(X1,X2,X3)) -> #mark(X1)
   #19: #U61(active(X)) -> #U61(X)
   #20: #mark(0()) -> #active(0())
   #21: #mark(U51(X1,X2,X3)) -> #active(U51(mark(X1),X2,X3))
   #22: #mark(U51(X1,X2,X3)) -> #U51(mark(X1),X2,X3)
   #23: #mark(U51(X1,X2,X3)) -> #mark(X1)
   #24: #U71(active(X1),X2,X3) -> #U71(X1,X2,X3)
   #25: #U71(X1,mark(X2),X3) -> #U71(X1,X2,X3)
   #26: #plus(X1,mark(X2)) -> #plus(X1,X2)
   #27: #U32(X1,mark(X2)) -> #U32(X1,X2)
   #28: #U11(X1,mark(X2),X3) -> #U11(X1,X2,X3)
   #29: #U12(X1,mark(X2)) -> #U12(X1,X2)
   #30: #U31(X1,X2,active(X3)) -> #U31(X1,X2,X3)
   #31: #U11(X1,X2,mark(X3)) -> #U11(X1,X2,X3)
   #32: #U32(X1,active(X2)) -> #U32(X1,X2)
   #33: #U32(active(X1),X2) -> #U32(X1,X2)
   #34: #U13(mark(X)) -> #U13(X)
   #35: #U21(X1,mark(X2)) -> #U21(X1,X2)
   #36: #mark(s(X)) -> #active(s(mark(X)))
   #37: #mark(s(X)) -> #s(mark(X))
   #38: #mark(s(X)) -> #mark(X)
   #39: #active(U31(tt(),V1,V2)) -> #mark(U32(isNat(V1),V2))
   #40: #active(U31(tt(),V1,V2)) -> #U32(isNat(V1),V2)
   #41: #active(U31(tt(),V1,V2)) -> #isNat(V1)
   #42: #U13(active(X)) -> #U13(X)
   #43: #isNatKind(mark(X)) -> #isNatKind(X)
   #44: #U12(X1,active(X2)) -> #U12(X1,X2)
   #45: #U31(X1,mark(X2),X3) -> #U31(X1,X2,X3)
   #46: #mark(U61(X)) -> #active(U61(mark(X)))
   #47: #mark(U61(X)) -> #U61(mark(X))
   #48: #mark(U61(X)) -> #mark(X)
   #49: #plus(mark(X1),X2) -> #plus(X1,X2)
   #50: #and(X1,mark(X2)) -> #and(X1,X2)
   #51: #U11(X1,X2,active(X3)) -> #U11(X1,X2,X3)
   #52: #active(and(tt(),X)) -> #mark(X)
   #53: #active(U41(tt(),N)) -> #mark(N)
   #54: #active(U61(tt())) -> #mark(0())
   #55: #U71(X1,X2,mark(X3)) -> #U71(X1,X2,X3)
   #56: #isNat(active(X)) -> #isNat(X)
   #57: #U33(mark(X)) -> #U33(X)
   #58: #and(X1,active(X2)) -> #and(X1,X2)
   #59: #U61(mark(X)) -> #U61(X)
   #60: #active(x(N,0())) -> #mark(U61(and(isNat(N),isNatKind(N))))
   #61: #active(x(N,0())) -> #U61(and(isNat(N),isNatKind(N)))
   #62: #active(x(N,0())) -> #and(isNat(N),isNatKind(N))
   #63: #active(x(N,0())) -> #isNat(N)
   #64: #active(x(N,0())) -> #isNatKind(N)
   #65: #U31(X1,active(X2),X3) -> #U31(X1,X2,X3)
   #66: #active(plus(N,s(M))) -> #mark(U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
   #67: #active(plus(N,s(M))) -> #U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)
   #68: #active(plus(N,s(M))) -> #and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))
   #69: #active(plus(N,s(M))) -> #and(isNat(M),isNatKind(M))
   #70: #active(plus(N,s(M))) -> #isNat(M)
   #71: #active(plus(N,s(M))) -> #isNatKind(M)
   #72: #active(plus(N,s(M))) -> #and(isNat(N),isNatKind(N))
   #73: #active(plus(N,s(M))) -> #isNat(N)
   #74: #active(plus(N,s(M))) -> #isNatKind(N)
   #75: #U41(X1,active(X2)) -> #U41(X1,X2)
   #76: #U41(mark(X1),X2) -> #U41(X1,X2)
   #77: #mark(isNatKind(X)) -> #active(isNatKind(X))
   #78: #U71(mark(X1),X2,X3) -> #U71(X1,X2,X3)
   #79: #U31(active(X1),X2,X3) -> #U31(X1,X2,X3)
   #80: #U71(X1,X2,active(X3)) -> #U71(X1,X2,X3)
   #81: #active(U71(tt(),M,N)) -> #mark(plus(x(N,M),N))
   #82: #active(U71(tt(),M,N)) -> #plus(x(N,M),N)
   #83: #active(U71(tt(),M,N)) -> #x(N,M)
   #84: #mark(U21(X1,X2)) -> #active(U21(mark(X1),X2))
   #85: #mark(U21(X1,X2)) -> #U21(mark(X1),X2)
   #86: #mark(U21(X1,X2)) -> #mark(X1)
   #87: #U41(X1,mark(X2)) -> #U41(X1,X2)
   #88: #isNat(mark(X)) -> #isNat(X)
   #89: #s(active(X)) -> #s(X)
   #90: #U51(mark(X1),X2,X3) -> #U51(X1,X2,X3)
   #91: #isNatKind(active(X)) -> #isNatKind(X)
   #92: #active(isNat(0())) -> #mark(tt())
   #93: #and(mark(X1),X2) -> #and(X1,X2)
   #94: #U21(active(X1),X2) -> #U21(X1,X2)
   #95: #mark(U13(X)) -> #active(U13(mark(X)))
   #96: #mark(U13(X)) -> #U13(mark(X))
   #97: #mark(U13(X)) -> #mark(X)
   #98: #U12(mark(X1),X2) -> #U12(X1,X2)
   #99: #U11(active(X1),X2,X3) -> #U11(X1,X2,X3)
   #100: #active(x(N,s(M))) -> #mark(U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N))
   #101: #active(x(N,s(M))) -> #U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)
   #102: #active(x(N,s(M))) -> #and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))
   #103: #active(x(N,s(M))) -> #and(isNat(M),isNatKind(M))
   #104: #active(x(N,s(M))) -> #isNat(M)
   #105: #active(x(N,s(M))) -> #isNatKind(M)
   #106: #active(x(N,s(M))) -> #and(isNat(N),isNatKind(N))
   #107: #active(x(N,s(M))) -> #isNat(N)
   #108: #active(x(N,s(M))) -> #isNatKind(N)
   #109: #and(active(X1),X2) -> #and(X1,X2)
   #110: #active(isNatKind(s(V1))) -> #mark(isNatKind(V1))
   #111: #active(isNatKind(s(V1))) -> #isNatKind(V1)
   #112: #s(mark(X)) -> #s(X)
   #113: #active(U32(tt(),V2)) -> #mark(U33(isNat(V2)))
   #114: #active(U32(tt(),V2)) -> #U33(isNat(V2))
   #115: #active(U32(tt(),V2)) -> #isNat(V2)
   #116: #mark(plus(X1,X2)) -> #active(plus(mark(X1),mark(X2)))
   #117: #mark(plus(X1,X2)) -> #plus(mark(X1),mark(X2))
   #118: #mark(plus(X1,X2)) -> #mark(X1)
   #119: #mark(plus(X1,X2)) -> #mark(X2)
   #120: #active(U51(tt(),M,N)) -> #mark(s(plus(N,M)))
   #121: #active(U51(tt(),M,N)) -> #s(plus(N,M))
   #122: #active(U51(tt(),M,N)) -> #plus(N,M)
   #123: #plus(active(X1),X2) -> #plus(X1,X2)
   #124: #plus(X1,active(X2)) -> #plus(X1,X2)
   #125: #U22(mark(X)) -> #U22(X)
   #126: #mark(U31(X1,X2,X3)) -> #active(U31(mark(X1),X2,X3))
   #127: #mark(U31(X1,X2,X3)) -> #U31(mark(X1),X2,X3)
   #128: #mark(U31(X1,X2,X3)) -> #mark(X1)
   #129: #U32(mark(X1),X2) -> #U32(X1,X2)
   #130: #active(U22(tt())) -> #mark(tt())
   #131: #mark(and(X1,X2)) -> #active(and(mark(X1),X2))
   #132: #mark(and(X1,X2)) -> #and(mark(X1),X2)
   #133: #mark(and(X1,X2)) -> #mark(X1)
   #134: #U22(active(X)) -> #U22(X)
   #135: #mark(U12(X1,X2)) -> #active(U12(mark(X1),X2))
   #136: #mark(U12(X1,X2)) -> #U12(mark(X1),X2)
   #137: #mark(U12(X1,X2)) -> #mark(X1)
   #138: #active(plus(N,0())) -> #mark(U41(and(isNat(N),isNatKind(N)),N))
   #139: #active(plus(N,0())) -> #U41(and(isNat(N),isNatKind(N)),N)
   #140: #active(plus(N,0())) -> #and(isNat(N),isNatKind(N))
   #141: #active(plus(N,0())) -> #isNat(N)
   #142: #active(plus(N,0())) -> #isNatKind(N)
   #143: #mark(U32(X1,X2)) -> #active(U32(mark(X1),X2))
   #144: #mark(U32(X1,X2)) -> #U32(mark(X1),X2)
   #145: #mark(U32(X1,X2)) -> #mark(X1)
   #146: #U51(X1,X2,mark(X3)) -> #U51(X1,X2,X3)
   #147: #U51(X1,X2,active(X3)) -> #U51(X1,X2,X3)
   #148: #mark(tt()) -> #active(tt())
   #149: #U21(mark(X1),X2) -> #U21(X1,X2)
   #150: #active(isNat(x(V1,V2))) -> #mark(U31(and(isNatKind(V1),isNatKind(V2)),V1,V2))
   #151: #active(isNat(x(V1,V2))) -> #U31(and(isNatKind(V1),isNatKind(V2)),V1,V2)
   #152: #active(isNat(x(V1,V2))) -> #and(isNatKind(V1),isNatKind(V2))
   #153: #active(isNat(x(V1,V2))) -> #isNatKind(V1)
   #154: #active(isNat(x(V1,V2))) -> #isNatKind(V2)
   #155: #mark(U22(X)) -> #active(U22(mark(X)))
   #156: #mark(U22(X)) -> #U22(mark(X))
   #157: #mark(U22(X)) -> #mark(X)
   #158: #active(isNatKind(plus(V1,V2))) -> #mark(and(isNatKind(V1),isNatKind(V2)))
   #159: #active(isNatKind(plus(V1,V2))) -> #and(isNatKind(V1),isNatKind(V2))
   #160: #active(isNatKind(plus(V1,V2))) -> #isNatKind(V1)
   #161: #active(isNatKind(plus(V1,V2))) -> #isNatKind(V2)
   #162: #U21(X1,active(X2)) -> #U21(X1,X2)
   #163: #x(X1,active(X2)) -> #x(X1,X2)
   #164: #mark(U11(X1,X2,X3)) -> #active(U11(mark(X1),X2,X3))
   #165: #mark(U11(X1,X2,X3)) -> #U11(mark(X1),X2,X3)
   #166: #mark(U11(X1,X2,X3)) -> #mark(X1)
   #167: #U71(X1,active(X2),X3) -> #U71(X1,X2,X3)
   #168: #U51(active(X1),X2,X3) -> #U51(X1,X2,X3)
   #169: #U31(X1,X2,mark(X3)) -> #U31(X1,X2,X3)
   #170: #mark(U41(X1,X2)) -> #active(U41(mark(X1),X2))
   #171: #mark(U41(X1,X2)) -> #U41(mark(X1),X2)
   #172: #mark(U41(X1,X2)) -> #mark(X1)
   #173: #active(isNatKind(x(V1,V2))) -> #mark(and(isNatKind(V1),isNatKind(V2)))
   #174: #active(isNatKind(x(V1,V2))) -> #and(isNatKind(V1),isNatKind(V2))
   #175: #active(isNatKind(x(V1,V2))) -> #isNatKind(V1)
   #176: #active(isNatKind(x(V1,V2))) -> #isNatKind(V2)
   #177: #active(isNat(s(V1))) -> #mark(U21(isNatKind(V1),V1))
   #178: #active(isNat(s(V1))) -> #U21(isNatKind(V1),V1)
   #179: #active(isNat(s(V1))) -> #isNatKind(V1)
   #180: #active(U13(tt())) -> #mark(tt())
   #181: #U33(active(X)) -> #U33(X)
   #182: #active(U11(tt(),V1,V2)) -> #mark(U12(isNat(V1),V2))
   #183: #active(U11(tt(),V1,V2)) -> #U12(isNat(V1),V2)
   #184: #active(U11(tt(),V1,V2)) -> #isNat(V1)
   #185: #U12(active(X1),X2) -> #U12(X1,X2)
   #186: #active(U33(tt())) -> #mark(tt())
   #187: #active(isNat(plus(V1,V2))) -> #mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2))
   #188: #active(isNat(plus(V1,V2))) -> #U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)
   #189: #active(isNat(plus(V1,V2))) -> #and(isNatKind(V1),isNatKind(V2))
   #190: #active(isNat(plus(V1,V2))) -> #isNatKind(V1)
   #191: #active(isNat(plus(V1,V2))) -> #isNatKind(V2)
   #192: #x(mark(X1),X2) -> #x(X1,X2)
   #193: #x(X1,mark(X2)) -> #x(X1,X2)
   #194: #active(U21(tt(),V1)) -> #mark(U22(isNat(V1)))
   #195: #active(U21(tt(),V1)) -> #U22(isNat(V1))
   #196: #active(U21(tt(),V1)) -> #isNat(V1)
   #197: #x(active(X1),X2) -> #x(X1,X2)
   #198: #U41(active(X1),X2) -> #U41(X1,X2)
   #199: #U11(X1,active(X2),X3) -> #U11(X1,X2,X3)
   #200: #active(isNatKind(0())) -> #mark(tt())
Number of SCCs: 19, DPs: 116, edges: 952
	SCC { #43 #91 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: x1
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #43 #91
Number of SCCs: 18, DPs: 114, edges: 948
	SCC { #56 #88 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: x1
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #56 #88
Number of SCCs: 17, DPs: 112, edges: 944
	SCC { #125 #134 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: x1
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #125 #134
Number of SCCs: 16, DPs: 110, edges: 940
	SCC { #34 #42 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: x1
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #34 #42
Number of SCCs: 15, DPs: 108, edges: 936
	SCC { #19 #59 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #19 #59
Number of SCCs: 14, DPs: 106, edges: 932
	SCC { #89 #112 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: x1
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #89 #112
Number of SCCs: 13, DPs: 104, edges: 928
	SCC { #57 #181 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: x1
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #57 #181
Number of SCCs: 12, DPs: 102, edges: 924
	SCC { #75 #76 #87 #198 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: x2
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #75 #87
Number of SCCs: 12, DPs: 100, edges: 912
	SCC { #76 #198 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: x1
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #76 #198
Number of SCCs: 11, DPs: 98, edges: 908
	SCC { #29 #44 #98 #185 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: x1
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #98 #185
Number of SCCs: 12, DPs: 96, edges: 896
	SCC { #29 #44 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: x2
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #29 #44
Number of SCCs: 11, DPs: 94, edges: 892
	SCC { #27 #32 #33 #129 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: x2
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #27 #32
Number of SCCs: 12, DPs: 92, edges: 880
	SCC { #33 #129 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: x1
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #33 #129
Number of SCCs: 11, DPs: 90, edges: 876
	SCC { #50 #58 #93 #109 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: x2
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #50 #58
Number of SCCs: 12, DPs: 88, edges: 864
	SCC { #93 #109 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: x1
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #93 #109
Number of SCCs: 11, DPs: 86, edges: 860
	SCC { #26 #49 #123 #124 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: x2
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #26 #124
Number of SCCs: 12, DPs: 84, edges: 848
	SCC { #49 #123 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: x1
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #49 #123
Number of SCCs: 11, DPs: 82, edges: 844
	SCC { #35 #94 #149 #162 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: x1
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #94 #149
Number of SCCs: 12, DPs: 80, edges: 832
	SCC { #35 #162 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: x2
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #35 #162
Number of SCCs: 11, DPs: 78, edges: 828
	SCC { #163 #192 #193 #197 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: x1
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #192 #197
Number of SCCs: 12, DPs: 76, edges: 816
	SCC { #163 #193 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: x2
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #163 #193
Number of SCCs: 11, DPs: 74, edges: 812
	SCC { #15 #28 #31 #51 #99 #199 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: x2 + x3
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #28 #31 #51 #199
Number of SCCs: 12, DPs: 70, edges: 780
	SCC { #15 #99 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: x1
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #15 #99
Number of SCCs: 11, DPs: 68, edges: 776
	SCC { #14 #30 #45 #65 #79 #169 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: x1 + x3
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #14 #30 #79 #169
Number of SCCs: 12, DPs: 64, edges: 744
	SCC { #45 #65 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: x2
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #45 #65
Number of SCCs: 11, DPs: 62, edges: 740
	SCC { #4 #13 #90 #146 #147 #168 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: x1 + x2
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #4 #13 #90 #168
Number of SCCs: 12, DPs: 58, edges: 708
	SCC { #146 #147 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: x3
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #146 #147
Number of SCCs: 11, DPs: 56, edges: 704
	SCC { #24 #25 #55 #78 #80 #167 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: x1 + x2
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #24 #25 #78 #167
Number of SCCs: 12, DPs: 52, edges: 672
	SCC { #55 #80 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2,x3)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: x3
   U13(x1)	weight: 0
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: 0
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #55 #80
Number of SCCs: 11, DPs: 50, edges: 668
	SCC { #1 #5 #7..9 #12 #16 #18 #21 #23 #38 #39 #48 #52 #53 #60 #66 #77 #81 #84 #86 #97 #100 #110 #113 #116 #118..120 #126 #128 #131 #133 #135 #137 #138 #143 #145 #150 #157 #158 #164 #166 #170 #172 #173 #177 #182 #187 #194 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8)
   U21(x1,x2)	weight: max{0, x1}
   U11(x1,x2,x3)	weight: max{0, x1}
     s(x1)	weight: x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: max{(/ 58723 4) + x3, (/ 3 8) + x2, (/ 1 2) + x1}
   and(x1,x2)	weight: max{x2, x1}
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: max{0, x1}
 #U33(x1)	weight: 0
     x(x1,x2)	weight: max{(/ 3 8) + x2, (/ 58723 4) + x1}
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: x1
   U32(x1,x2)	weight: max{0, x1}
   U33(x1)	weight: x1
 isNat(x1)	weight: (/ 1 8)
  plus(x1,x2)	weight: max{(/ 58723 4) + x2, x1}
   U61(x1)	weight: (/ 1 8) + x1
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: x1
   U31(x1,x2,x3)	weight: max{0, x1}
 #U41(x1,x2)	weight: 0
#active(x1)	weight: x1
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: (/ 1 8)
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: x1
   U22(x1)	weight: x1
   U51(x1,x2,x3)	weight: max{x3, (/ 58723 4) + x2, (/ 1 8) + x1}
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: max{x2, (/ 117445 8) + x1}
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { 1..111 }
    Removed DPs: #7 #8 #18 #23 #48 #60 #119 #172
Number of SCCs: 12, DPs: 42, edges: 354
	SCC { #1 #5 #9 #12 #16 #21 #38 #39 #52 #53 #66 #77 #81 #84 #86 #97 #100 #110 #113 #116 #118 #120 #126 #128 #131 #133 #135 #137 #138 #143 #145 #150 #157 #158 #164 #166 #170 #173 #177 #182 #187 #194 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: 23505
   U21(x1,x2)	weight: max{(/ 70649 2) + x2, (/ 1 4) + x1}
   U11(x1,x2,x3)	weight: max{(/ 70649 2) + x3, (/ 70649 2) + x2, (/ 47277 4) + x1}
     s(x1)	weight: x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: max{58829 + x3, (/ 235317 4) + x2, (/ 1 4) + x1}
   and(x1,x2)	weight: max{x2, x1}
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: max{(/ 70649 2) + x2, x1}
 #U33(x1)	weight: 0
     x(x1,x2)	weight: max{(/ 235317 4) + x2, 58829 + x1}
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: x1
   U32(x1,x2)	weight: max{35325 + x2, (/ 141299 4) + x1}
   U33(x1)	weight: (/ 1 4) + x1
 isNat(x1)	weight: (/ 70649 2) + x1
  plus(x1,x2)	weight: max{58829 + x2, x1}
   U61(x1)	weight: x1
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: x1
   U31(x1,x2,x3)	weight: max{(/ 141297 2) + x3, (/ 188307 2) + x2, (/ 282595 4) + x1}
 #U41(x1,x2)	weight: 0
#active(x1)	weight: x1
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: (/ 1 4)
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: x1
   U22(x1)	weight: x1
   U51(x1,x2,x3)	weight: max{0, x3, 58829 + x2}
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: max{0, x2}
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { 1..111 }
    Removed DPs: #12 #39 #86 #113 #128 #145 #166
Number of SCCs: 12, DPs: 32, edges: 168
	SCC { #1 #5 #9 #16 #21 #38 #52 #53 #66 #77 #81 #84 #97 #100 #110 #116 #118 #120 #131 #133 #135 #137 #138 #157 #158 #164 #170 #173 #177 #182 #187 #194 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 164267 8)
   U21(x1,x2)	weight: max{(/ 164269 8) + x2, (/ 1 8) + x1}
   U11(x1,x2,x3)	weight: max{(/ 82135 4) + x3, (/ 164269 8) + x2, 20534 + x1}
     s(x1)	weight: x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: max{(/ 82135 4) + x3, (/ 164271 8) + x2, (/ 1 8) + x1}
   and(x1,x2)	weight: max{x2, x1}
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: max{(/ 82135 4) + x2, x1}
 #U33(x1)	weight: 0
     x(x1,x2)	weight: max{(/ 164271 8) + x2, (/ 82135 4) + x1}
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: x1
   U32(x1,x2)	weight: max{(/ 164271 8) + x2, (/ 82135 4) + x1}
   U33(x1)	weight: (/ 1 8) + x1
 isNat(x1)	weight: (/ 164269 8) + x1
  plus(x1,x2)	weight: max{(/ 82135 4) + x2, x1}
   U61(x1)	weight: x1
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: x1
   U31(x1,x2,x3)	weight: max{(/ 164271 8) + x3, (/ 328539 8) + x2, (/ 164273 8) + x1}
 #U41(x1,x2)	weight: 0
#active(x1)	weight: x1
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: (/ 164265 8)
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: (/ 1 8) + x1
   U22(x1)	weight: x1
   U51(x1,x2,x3)	weight: max{0, x3, (/ 82135 4) + x2}
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: max{0, x2}
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { 1..111 }
    Removed DPs: #97
Number of SCCs: 12, DPs: 29, edges: 134
	SCC { #5 #9 #16 #21 #38 #52 #53 #66 #77 #81 #84 #100 #110 #116 #118 #120 #131 #133 #137 #138 #157 #158 #164 #170 #173 #177 #182 #187 #194 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 32) + x1
   U21(x1,x2)	weight: max{(/ 3 16) + x2, (/ 1 8) + x1}
   U11(x1,x2,x3)	weight: max{(/ 11 32) + x3, (/ 3 16) + x2, (/ 5 32) + x1}
     s(x1)	weight: x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: max{(/ 7 16) + x3, (/ 15 32) + x2, (/ 3 32) + x1}
   and(x1,x2)	weight: max{(/ 1 8) + x2, x1}
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: max{(/ 7 32) + x2, x1}
 #U33(x1)	weight: 0
     x(x1,x2)	weight: max{(/ 15 32) + x2, (/ 7 16) + x1}
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: x1
     0()	weight: (/ 1 16)
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: x1
   U32(x1,x2)	weight: max{(/ 15 32) + x2, (/ 7 16) + x1}
   U33(x1)	weight: (/ 1 32) + x1
 isNat(x1)	weight: (/ 3 16) + x1
  plus(x1,x2)	weight: max{(/ 5 32) + x2, x1}
   U61(x1)	weight: x1
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: x1
   U31(x1,x2,x3)	weight: max{(/ 15 32) + x3, (/ 5 8) + x2, (/ 1 2) + x1}
 #U41(x1,x2)	weight: 0
#active(x1)	weight: x1
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: (/ 3 32)
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: (/ 1 32) + x1
   U22(x1)	weight: x1
   U51(x1,x2,x3)	weight: max{0, x3, (/ 5 32) + x2}
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: max{0, x2}
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { 1..111 }
    Removed DPs: #52 #173
Number of SCCs: 12, DPs: 26, edges: 108
	SCC { #5 #9 #16 #21 #38 #53 #66 #77 #81 #84 #100 #110 #116 #118 #120 #133 #137 #138 #157 #158 #164 #170 #177 #182 #187 #194 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
 #U32(x1,x2)	status: []	precedence above:
isNatKind(x1)	status: [x1]	precedence above: and #mark #active tt
   U21(x1,x2)	status: x2
   U11(x1,x2,x3)	status: [x2,x1]	precedence above: s and U12 #mark isNat U31 #active tt U13
     s(x1)	status: [x1]	precedence above: isNat U31
#isNat(x1)	status: []	precedence above:
   U71(x1,x2,x3)	status: [x2,x3,x1]	precedence above: isNatKind U11 s and U12 x #mark 0 isNat plus U61 U31 #active tt U13 U51 U41
   and(x1,x2)	status: [x2,x1]	precedence above:
#plus(x1,x2)	status: [x2]	precedence above:
 #U13(x1)	status: []	precedence above:
   U12(x1,x2)	status: [x1]	precedence above: U11 s and #mark isNat U31 #active tt U13
 #U33(x1)	status: []	precedence above:
     x(x1,x2)	status: [x2,x1]	precedence above: isNatKind U11 s U71 and U12 #mark 0 isNat plus U61 U31 #active tt U13 U51 U41
 #U12(x1,x2)	status: [x2]	precedence above:
#mark(x1)	status: [x1]	precedence above: and #active
     0()	status: []	precedence above: and #mark U61 #active tt
   #x(x1,x2)	status: [x2]	precedence above:
   #s(x1)	status: []	precedence above:
  mark(x1)	status: x1
   U32(x1,x2)	status: x2
   U33(x1)	status: x1
 isNat(x1)	status: x1
  plus(x1,x2)	status: [x1,x2]	precedence above: isNatKind U11 s and U12 #mark isNat U31 #active tt U13 U51 U41
   U61(x1)	status: []	precedence above: and #mark 0 #active tt
 #U51(x1,x2,x3)	status: []	precedence above:
 #U11(x1,x2,x3)	status: []	precedence above:
active(x1)	status: x1
   U31(x1,x2,x3)	status: x3
 #U41(x1,x2)	status: [x1,x2]	precedence above:
#active(x1)	status: [x1]	precedence above: and #mark
 #U21(x1,x2)	status: [x1]	precedence above:
 #U22(x1)	status: []	precedence above:
    tt()	status: []	precedence above: and #mark #active
 #U71(x1,x2,x3)	status: [x2]	precedence above:
   U13(x1)	status: []	precedence above: U11 s and U12 #mark isNat U31 #active tt
   U22(x1)	status: x1
   U51(x1,x2,x3)	status: [x3,x2,x1]	precedence above: isNatKind U11 s and U12 #mark isNat plus U31 #active tt U13 U41
#isNatKind(x1)	status: []	precedence above:
   U41(x1,x2)	status: [x2]	precedence above: and #mark #active
 #U31(x1,x2,x3)	status: [x3,x1,x2]	precedence above:
 #and(x1,x2)	status: [x1,x2]	precedence above:
 #U61(x1)	status: []	precedence above:
    Usable rules: { 1..111 }
    Removed DPs: #38 #53 #81 #100 #110 #118 #133 #137 #138 #158 #182 #187
Number of SCCs: 12, DPs: 5, edges: 7
	SCC { #9 #84 #157 #177 #194 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8)
   U21(x1,x2)	weight: (/ 1 2) + x2
   U11(x1,x2,x3)	weight: (/ 1 2) + x2
     s(x1)	weight: (/ 5 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 3 8)
   and(x1,x2)	weight: (/ 3 8)
#plus(x1,x2)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: (/ 3 4) + x2
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8)
 #U12(x1,x2)	weight: 0
#mark(x1)	weight: (/ 1 8) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 8) + x1
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8)
   U61(x1)	weight: x1
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 1 4) + x1
   U31(x1,x2,x3)	weight: (/ 1 2) + x2
 #U41(x1,x2)	weight: 0
#active(x1)	weight: x1
 #U21(x1,x2)	weight: 0
 #U22(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U13(x1)	weight: x1
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 3 8)
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { 46..57 60..63 66..75 78..87 90..93 96..111 }
    Removed DPs: #9 #84 #157 #177 #194
Number of SCCs: 11, DPs: 0, edges: 0
YES