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: active(U11(X1,X2,X3)) -> U11(active(X1),X2,X3)
    27: active(U12(X1,X2)) -> U12(active(X1),X2)
    28: active(U13(X)) -> U13(active(X))
    29: active(U21(X1,X2)) -> U21(active(X1),X2)
    30: active(U22(X)) -> U22(active(X))
    31: active(U31(X1,X2,X3)) -> U31(active(X1),X2,X3)
    32: active(U32(X1,X2)) -> U32(active(X1),X2)
    33: active(U33(X)) -> U33(active(X))
    34: active(U41(X1,X2)) -> U41(active(X1),X2)
    35: active(U51(X1,X2,X3)) -> U51(active(X1),X2,X3)
    36: active(s(X)) -> s(active(X))
    37: active(plus(X1,X2)) -> plus(active(X1),X2)
    38: active(plus(X1,X2)) -> plus(X1,active(X2))
    39: active(U61(X)) -> U61(active(X))
    40: active(U71(X1,X2,X3)) -> U71(active(X1),X2,X3)
    41: active(x(X1,X2)) -> x(active(X1),X2)
    42: active(x(X1,X2)) -> x(X1,active(X2))
    43: active(and(X1,X2)) -> and(active(X1),X2)
    44: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3))
    45: U12(mark(X1),X2) -> mark(U12(X1,X2))
    46: U13(mark(X)) -> mark(U13(X))
    47: U21(mark(X1),X2) -> mark(U21(X1,X2))
    48: U22(mark(X)) -> mark(U22(X))
    49: U31(mark(X1),X2,X3) -> mark(U31(X1,X2,X3))
    50: U32(mark(X1),X2) -> mark(U32(X1,X2))
    51: U33(mark(X)) -> mark(U33(X))
    52: U41(mark(X1),X2) -> mark(U41(X1,X2))
    53: U51(mark(X1),X2,X3) -> mark(U51(X1,X2,X3))
    54: s(mark(X)) -> mark(s(X))
    55: plus(mark(X1),X2) -> mark(plus(X1,X2))
    56: plus(X1,mark(X2)) -> mark(plus(X1,X2))
    57: U61(mark(X)) -> mark(U61(X))
    58: U71(mark(X1),X2,X3) -> mark(U71(X1,X2,X3))
    59: x(mark(X1),X2) -> mark(x(X1,X2))
    60: x(X1,mark(X2)) -> mark(x(X1,X2))
    61: and(mark(X1),X2) -> mark(and(X1,X2))
    62: proper(U11(X1,X2,X3)) -> U11(proper(X1),proper(X2),proper(X3))
    63: proper(tt()) -> ok(tt())
    64: proper(U12(X1,X2)) -> U12(proper(X1),proper(X2))
    65: proper(isNat(X)) -> isNat(proper(X))
    66: proper(U13(X)) -> U13(proper(X))
    67: proper(U21(X1,X2)) -> U21(proper(X1),proper(X2))
    68: proper(U22(X)) -> U22(proper(X))
    69: proper(U31(X1,X2,X3)) -> U31(proper(X1),proper(X2),proper(X3))
    70: proper(U32(X1,X2)) -> U32(proper(X1),proper(X2))
    71: proper(U33(X)) -> U33(proper(X))
    72: proper(U41(X1,X2)) -> U41(proper(X1),proper(X2))
    73: proper(U51(X1,X2,X3)) -> U51(proper(X1),proper(X2),proper(X3))
    74: proper(s(X)) -> s(proper(X))
    75: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
    76: proper(U61(X)) -> U61(proper(X))
    77: proper(0()) -> ok(0())
    78: proper(U71(X1,X2,X3)) -> U71(proper(X1),proper(X2),proper(X3))
    79: proper(x(X1,X2)) -> x(proper(X1),proper(X2))
    80: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
    81: proper(isNatKind(X)) -> isNatKind(proper(X))
    82: U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3))
    83: U12(ok(X1),ok(X2)) -> ok(U12(X1,X2))
    84: isNat(ok(X)) -> ok(isNat(X))
    85: U13(ok(X)) -> ok(U13(X))
    86: U21(ok(X1),ok(X2)) -> ok(U21(X1,X2))
    87: U22(ok(X)) -> ok(U22(X))
    88: U31(ok(X1),ok(X2),ok(X3)) -> ok(U31(X1,X2,X3))
    89: U32(ok(X1),ok(X2)) -> ok(U32(X1,X2))
    90: U33(ok(X)) -> ok(U33(X))
    91: U41(ok(X1),ok(X2)) -> ok(U41(X1,X2))
    92: U51(ok(X1),ok(X2),ok(X3)) -> ok(U51(X1,X2,X3))
    93: s(ok(X)) -> ok(s(X))
    94: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
    95: U61(ok(X)) -> ok(U61(X))
    96: U71(ok(X1),ok(X2),ok(X3)) -> ok(U71(X1,X2,X3))
    97: x(ok(X1),ok(X2)) -> ok(x(X1,X2))
    98: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
    99: isNatKind(ok(X)) -> ok(isNatKind(X))
    100: top(mark(X)) -> top(proper(X))
    101: top(ok(X)) -> top(active(X))
Number of strict rules: 101
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(U12(tt(),V2)) -> #U13(isNat(V2))
   #2: #active(U12(tt(),V2)) -> #isNat(V2)
   #3: #U21(ok(X1),ok(X2)) -> #U21(X1,X2)
   #4: #active(and(X1,X2)) -> #and(active(X1),X2)
   #5: #active(and(X1,X2)) -> #active(X1)
   #6: #active(U21(X1,X2)) -> #U21(active(X1),X2)
   #7: #active(U21(X1,X2)) -> #active(X1)
   #8: #active(U51(X1,X2,X3)) -> #U51(active(X1),X2,X3)
   #9: #active(U51(X1,X2,X3)) -> #active(X1)
   #10: #U12(ok(X1),ok(X2)) -> #U12(X1,X2)
   #11: #proper(U13(X)) -> #U13(proper(X))
   #12: #proper(U13(X)) -> #proper(X)
   #13: #U13(mark(X)) -> #U13(X)
   #14: #active(x(X1,X2)) -> #x(X1,active(X2))
   #15: #active(x(X1,X2)) -> #active(X2)
   #16: #U61(ok(X)) -> #U61(X)
   #17: #active(x(X1,X2)) -> #x(active(X1),X2)
   #18: #active(x(X1,X2)) -> #active(X1)
   #19: #active(plus(X1,X2)) -> #plus(active(X1),X2)
   #20: #active(plus(X1,X2)) -> #active(X1)
   #21: #isNatKind(ok(X)) -> #isNatKind(X)
   #22: #x(ok(X1),ok(X2)) -> #x(X1,X2)
   #23: #U41(ok(X1),ok(X2)) -> #U41(X1,X2)
   #24: #proper(U51(X1,X2,X3)) -> #U51(proper(X1),proper(X2),proper(X3))
   #25: #proper(U51(X1,X2,X3)) -> #proper(X1)
   #26: #proper(U51(X1,X2,X3)) -> #proper(X2)
   #27: #proper(U51(X1,X2,X3)) -> #proper(X3)
   #28: #U21(mark(X1),X2) -> #U21(X1,X2)
   #29: #U51(mark(X1),X2,X3) -> #U51(X1,X2,X3)
   #30: #proper(U33(X)) -> #U33(proper(X))
   #31: #proper(U33(X)) -> #proper(X)
   #32: #U22(mark(X)) -> #U22(X)
   #33: #proper(plus(X1,X2)) -> #plus(proper(X1),proper(X2))
   #34: #proper(plus(X1,X2)) -> #proper(X1)
   #35: #proper(plus(X1,X2)) -> #proper(X2)
   #36: #proper(s(X)) -> #s(proper(X))
   #37: #proper(s(X)) -> #proper(X)
   #38: #U71(mark(X1),X2,X3) -> #U71(X1,X2,X3)
   #39: #and(mark(X1),X2) -> #and(X1,X2)
   #40: #active(plus(X1,X2)) -> #plus(X1,active(X2))
   #41: #active(plus(X1,X2)) -> #active(X2)
   #42: #active(U31(tt(),V1,V2)) -> #U32(isNat(V1),V2)
   #43: #active(U31(tt(),V1,V2)) -> #isNat(V1)
   #44: #x(mark(X1),X2) -> #x(X1,X2)
   #45: #plus(mark(X1),X2) -> #plus(X1,X2)
   #46: #proper(U21(X1,X2)) -> #U21(proper(X1),proper(X2))
   #47: #proper(U21(X1,X2)) -> #proper(X1)
   #48: #proper(U21(X1,X2)) -> #proper(X2)
   #49: #active(U71(X1,X2,X3)) -> #U71(active(X1),X2,X3)
   #50: #active(U71(X1,X2,X3)) -> #active(X1)
   #51: #U33(ok(X)) -> #U33(X)
   #52: #U33(mark(X)) -> #U33(X)
   #53: #and(ok(X1),ok(X2)) -> #and(X1,X2)
   #54: #U61(mark(X)) -> #U61(X)
   #55: #proper(U61(X)) -> #U61(proper(X))
   #56: #proper(U61(X)) -> #proper(X)
   #57: #plus(ok(X1),ok(X2)) -> #plus(X1,X2)
   #58: #active(x(N,0())) -> #U61(and(isNat(N),isNatKind(N)))
   #59: #active(x(N,0())) -> #and(isNat(N),isNatKind(N))
   #60: #active(x(N,0())) -> #isNat(N)
   #61: #active(x(N,0())) -> #isNatKind(N)
   #62: #proper(U32(X1,X2)) -> #U32(proper(X1),proper(X2))
   #63: #proper(U32(X1,X2)) -> #proper(X1)
   #64: #proper(U32(X1,X2)) -> #proper(X2)
   #65: #active(plus(N,s(M))) -> #U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)
   #66: #active(plus(N,s(M))) -> #and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))
   #67: #active(plus(N,s(M))) -> #and(isNat(M),isNatKind(M))
   #68: #active(plus(N,s(M))) -> #isNat(M)
   #69: #active(plus(N,s(M))) -> #isNatKind(M)
   #70: #active(plus(N,s(M))) -> #and(isNat(N),isNatKind(N))
   #71: #active(plus(N,s(M))) -> #isNat(N)
   #72: #active(plus(N,s(M))) -> #isNatKind(N)
   #73: #proper(isNatKind(X)) -> #isNatKind(proper(X))
   #74: #proper(isNatKind(X)) -> #proper(X)
   #75: #proper(U71(X1,X2,X3)) -> #U71(proper(X1),proper(X2),proper(X3))
   #76: #proper(U71(X1,X2,X3)) -> #proper(X1)
   #77: #proper(U71(X1,X2,X3)) -> #proper(X2)
   #78: #proper(U71(X1,X2,X3)) -> #proper(X3)
   #79: #U12(mark(X1),X2) -> #U12(X1,X2)
   #80: #U71(ok(X1),ok(X2),ok(X3)) -> #U71(X1,X2,X3)
   #81: #proper(U31(X1,X2,X3)) -> #U31(proper(X1),proper(X2),proper(X3))
   #82: #proper(U31(X1,X2,X3)) -> #proper(X1)
   #83: #proper(U31(X1,X2,X3)) -> #proper(X2)
   #84: #proper(U31(X1,X2,X3)) -> #proper(X3)
   #85: #top(ok(X)) -> #top(active(X))
   #86: #top(ok(X)) -> #active(X)
   #87: #active(U71(tt(),M,N)) -> #plus(x(N,M),N)
   #88: #active(U71(tt(),M,N)) -> #x(N,M)
   #89: #active(U31(X1,X2,X3)) -> #U31(active(X1),X2,X3)
   #90: #active(U31(X1,X2,X3)) -> #active(X1)
   #91: #proper(x(X1,X2)) -> #x(proper(X1),proper(X2))
   #92: #proper(x(X1,X2)) -> #proper(X1)
   #93: #proper(x(X1,X2)) -> #proper(X2)
   #94: #plus(X1,mark(X2)) -> #plus(X1,X2)
   #95: #U32(ok(X1),ok(X2)) -> #U32(X1,X2)
   #96: #U11(ok(X1),ok(X2),ok(X3)) -> #U11(X1,X2,X3)
   #97: #proper(U11(X1,X2,X3)) -> #U11(proper(X1),proper(X2),proper(X3))
   #98: #proper(U11(X1,X2,X3)) -> #proper(X1)
   #99: #proper(U11(X1,X2,X3)) -> #proper(X2)
   #100: #proper(U11(X1,X2,X3)) -> #proper(X3)
   #101: #active(U22(X)) -> #U22(active(X))
   #102: #active(U22(X)) -> #active(X)
   #103: #U41(mark(X1),X2) -> #U41(X1,X2)
   #104: #U31(mark(X1),X2,X3) -> #U31(X1,X2,X3)
   #105: #active(x(N,s(M))) -> #U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)
   #106: #active(x(N,s(M))) -> #and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))
   #107: #active(x(N,s(M))) -> #and(isNat(M),isNatKind(M))
   #108: #active(x(N,s(M))) -> #isNat(M)
   #109: #active(x(N,s(M))) -> #isNatKind(M)
   #110: #active(x(N,s(M))) -> #and(isNat(N),isNatKind(N))
   #111: #active(x(N,s(M))) -> #isNat(N)
   #112: #active(x(N,s(M))) -> #isNatKind(N)
   #113: #active(isNatKind(s(V1))) -> #isNatKind(V1)
   #114: #U31(ok(X1),ok(X2),ok(X3)) -> #U31(X1,X2,X3)
   #115: #active(U32(tt(),V2)) -> #U33(isNat(V2))
   #116: #active(U32(tt(),V2)) -> #isNat(V2)
   #117: #active(U61(X)) -> #U61(active(X))
   #118: #active(U61(X)) -> #active(X)
   #119: #active(U51(tt(),M,N)) -> #s(plus(N,M))
   #120: #active(U51(tt(),M,N)) -> #plus(N,M)
   #121: #U51(ok(X1),ok(X2),ok(X3)) -> #U51(X1,X2,X3)
   #122: #s(ok(X)) -> #s(X)
   #123: #proper(U12(X1,X2)) -> #U12(proper(X1),proper(X2))
   #124: #proper(U12(X1,X2)) -> #proper(X1)
   #125: #proper(U12(X1,X2)) -> #proper(X2)
   #126: #active(U33(X)) -> #U33(active(X))
   #127: #active(U33(X)) -> #active(X)
   #128: #proper(U41(X1,X2)) -> #U41(proper(X1),proper(X2))
   #129: #proper(U41(X1,X2)) -> #proper(X1)
   #130: #proper(U41(X1,X2)) -> #proper(X2)
   #131: #U11(mark(X1),X2,X3) -> #U11(X1,X2,X3)
   #132: #proper(isNat(X)) -> #isNat(proper(X))
   #133: #proper(isNat(X)) -> #proper(X)
   #134: #active(U13(X)) -> #U13(active(X))
   #135: #active(U13(X)) -> #active(X)
   #136: #active(plus(N,0())) -> #U41(and(isNat(N),isNatKind(N)),N)
   #137: #active(plus(N,0())) -> #and(isNat(N),isNatKind(N))
   #138: #active(plus(N,0())) -> #isNat(N)
   #139: #active(plus(N,0())) -> #isNatKind(N)
   #140: #active(U41(X1,X2)) -> #U41(active(X1),X2)
   #141: #active(U41(X1,X2)) -> #active(X1)
   #142: #isNat(ok(X)) -> #isNat(X)
   #143: #U22(ok(X)) -> #U22(X)
   #144: #active(U12(X1,X2)) -> #U12(active(X1),X2)
   #145: #active(U12(X1,X2)) -> #active(X1)
   #146: #x(X1,mark(X2)) -> #x(X1,X2)
   #147: #active(isNat(x(V1,V2))) -> #U31(and(isNatKind(V1),isNatKind(V2)),V1,V2)
   #148: #active(isNat(x(V1,V2))) -> #and(isNatKind(V1),isNatKind(V2))
   #149: #active(isNat(x(V1,V2))) -> #isNatKind(V1)
   #150: #active(isNat(x(V1,V2))) -> #isNatKind(V2)
   #151: #active(U32(X1,X2)) -> #U32(active(X1),X2)
   #152: #active(U32(X1,X2)) -> #active(X1)
   #153: #active(isNatKind(plus(V1,V2))) -> #and(isNatKind(V1),isNatKind(V2))
   #154: #active(isNatKind(plus(V1,V2))) -> #isNatKind(V1)
   #155: #active(isNatKind(plus(V1,V2))) -> #isNatKind(V2)
   #156: #active(U11(X1,X2,X3)) -> #U11(active(X1),X2,X3)
   #157: #active(U11(X1,X2,X3)) -> #active(X1)
   #158: #top(mark(X)) -> #top(proper(X))
   #159: #top(mark(X)) -> #proper(X)
   #160: #U13(ok(X)) -> #U13(X)
   #161: #proper(U22(X)) -> #U22(proper(X))
   #162: #proper(U22(X)) -> #proper(X)
   #163: #active(s(X)) -> #s(active(X))
   #164: #active(s(X)) -> #active(X)
   #165: #active(isNatKind(x(V1,V2))) -> #and(isNatKind(V1),isNatKind(V2))
   #166: #active(isNatKind(x(V1,V2))) -> #isNatKind(V1)
   #167: #active(isNatKind(x(V1,V2))) -> #isNatKind(V2)
   #168: #active(isNat(s(V1))) -> #U21(isNatKind(V1),V1)
   #169: #active(isNat(s(V1))) -> #isNatKind(V1)
   #170: #active(U11(tt(),V1,V2)) -> #U12(isNat(V1),V2)
   #171: #active(U11(tt(),V1,V2)) -> #isNat(V1)
   #172: #s(mark(X)) -> #s(X)
   #173: #active(isNat(plus(V1,V2))) -> #U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)
   #174: #active(isNat(plus(V1,V2))) -> #and(isNatKind(V1),isNatKind(V2))
   #175: #active(isNat(plus(V1,V2))) -> #isNatKind(V1)
   #176: #active(isNat(plus(V1,V2))) -> #isNatKind(V2)
   #177: #active(U21(tt(),V1)) -> #U22(isNat(V1))
   #178: #active(U21(tt(),V1)) -> #isNat(V1)
   #179: #proper(and(X1,X2)) -> #and(proper(X1),proper(X2))
   #180: #proper(and(X1,X2)) -> #proper(X1)
   #181: #proper(and(X1,X2)) -> #proper(X2)
   #182: #U32(mark(X1),X2) -> #U32(X1,X2)
Number of SCCs: 21, DPs: 89, edges: 1493
	SCC { #142 }
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
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #top(x1)	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
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: 0
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
#proper(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: 0
   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: #142
Number of SCCs: 20, DPs: 88, edges: 1492
	SCC { #21 }
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
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #top(x1)	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
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: 0
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
#proper(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: 0
   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: #21
Number of SCCs: 19, DPs: 87, edges: 1491
	SCC { #32 #143 }
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
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #top(x1)	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
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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
#proper(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: 0
   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: #32 #143
Number of SCCs: 18, DPs: 85, edges: 1487
	SCC { #122 #172 }
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
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #top(x1)	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
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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
#proper(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: 0
   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: #122 #172
Number of SCCs: 17, DPs: 83, edges: 1483
	SCC { #13 #160 }
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
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #top(x1)	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
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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
#proper(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: 0
   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: #13 #160
Number of SCCs: 16, DPs: 81, edges: 1479
	SCC { #51 #52 }
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
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #top(x1)	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
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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
#proper(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: 0
   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: #51 #52
Number of SCCs: 15, DPs: 79, edges: 1475
	SCC { #16 #54 }
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
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #top(x1)	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
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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
#proper(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: 0
   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: #16 #54
Number of SCCs: 14, DPs: 77, edges: 1471
	SCC { #85 #158 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
 #U32(x1,x2)	status: [x2]	precedence above:
isNatKind(x1)	status: x1
   U21(x1,x2)	status: [x2,x1]	precedence above: and mark U33 isNat tt U13 U22
   U11(x1,x2,x3)	status: [x2,x1,x3]	precedence above: and U12 mark U33 isNat U13
     s(x1)	status: [x1]	precedence above: U21 and mark U33 isNat tt U13 U22
#isNat(x1)	status: []	precedence above:
   U71(x1,x2,x3)	status: [x3,x2,x1]	precedence above: U21 U11 s and U12 x 0 mark U32 U33 isNat plus U61 U31 tt U13 U22 U51 U41
   top(x1)	status: []	precedence above:
   and(x1,x2)	status: [x2,x1]	precedence above: mark U33
#plus(x1,x2)	status: [x2]	precedence above:
 #top(x1)	status: [x1]	precedence above:
 #U13(x1)	status: []	precedence above:
   U12(x1,x2)	status: [x1,x2]	precedence above: and mark U33 isNat U13
 #U33(x1)	status: []	precedence above:
     x(x1,x2)	status: [x1,x2]	precedence above: U21 U11 s U71 and U12 0 mark U32 U33 isNat plus U61 U31 tt U13 U22 U51 U41
 #U12(x1,x2)	status: [x2]	precedence above:
proper(x1)	status: x1
    ok(x1)	status: x1
     0()	status: []	precedence above: mark U33 tt
   #x(x1,x2)	status: [x1]	precedence above:
   #s(x1)	status: []	precedence above:
  mark(x1)	status: [x1]	precedence above: U33
   U32(x1,x2)	status: [x2,x1]	precedence above: and mark U33 isNat
   U33(x1)	status: [x1]	precedence above: mark
#proper(x1)	status: []	precedence above:
 isNat(x1)	status: [x1]	precedence above: and mark U33
  plus(x1,x2)	status: [x1,x2]	precedence above: U21 U11 s and U12 mark U33 isNat tt U13 U22 U51 U41
   U61(x1)	status: [x1]	precedence above: 0 mark U33 tt
 #U51(x1,x2,x3)	status: [x2,x3,x1]	precedence above:
 #U11(x1,x2,x3)	status: [x2,x1,x3]	precedence above:
active(x1)	status: x1
   U31(x1,x2,x3)	status: [x2,x1,x3]	precedence above: and mark U32 U33 isNat
 #U41(x1,x2)	status: [x1]	precedence above:
#active(x1)	status: []	precedence above:
 #U21(x1,x2)	status: [x2]	precedence above:
 #U22(x1)	status: []	precedence above:
    tt()	status: []	precedence above:
 #U71(x1,x2,x3)	status: [x1,x3]	precedence above:
   U13(x1)	status: [x1]	precedence above: mark U33
   U22(x1)	status: [x1]	precedence above: mark U33 tt
   U51(x1,x2,x3)	status: [x3,x2,x1]	precedence above: U21 U11 s and U12 mark U33 isNat plus tt U13 U22 U41
#isNatKind(x1)	status: []	precedence above:
   U41(x1,x2)	status: [x1,x2]	precedence above: mark U33
 #U31(x1,x2,x3)	status: [x1]	precedence above:
 #and(x1,x2)	status: [x2]	precedence above:
 #U61(x1)	status: []	precedence above:
    Usable rules: { 1..99 }
    Removed DPs: #158
Number of SCCs: 14, DPs: 76, edges: 1468
	SCC { #85 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 4) + x1
   U21(x1,x2)	weight: (/ 1 4) + x2
   U11(x1,x2,x3)	weight: (/ 1 4) + x1
     s(x1)	weight: (/ 1 4) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 4) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: x1
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: (/ 1 4) + x2
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 4) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4)
   U32(x1,x2)	weight: (/ 1 4) + x2
   U33(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 4) + x1
  plus(x1,x2)	weight: (/ 1 4) + x1
   U61(x1)	weight: (/ 1 4) + 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 4) + x3
 #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: (/ 1 4) + x1
   U22(x1)	weight: (/ 1 4) + x1
   U51(x1,x2,x3)	weight: (/ 1 4) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 4) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { 1..61 82..99 }
    Removed DPs: #85
Number of SCCs: 13, DPs: 75, edges: 1467
	SCC { #39 #53 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 4) + x1
   U21(x1,x2)	weight: (/ 1 4) + x2
   U11(x1,x2,x3)	weight: (/ 1 4) + x1
     s(x1)	weight: (/ 1 4) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 4) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: x1
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: (/ 1 4) + x2
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 4) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4)
   U32(x1,x2)	weight: (/ 1 4) + x2
   U33(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 4) + x1
  plus(x1,x2)	weight: (/ 1 4) + x1
   U61(x1)	weight: (/ 1 4) + 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 4) + x3
 #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: (/ 1 4) + x1
   U22(x1)	weight: (/ 1 4) + x1
   U51(x1,x2,x3)	weight: (/ 1 4) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 4) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: x2
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #53
Number of SCCs: 14, DPs: 74, edges: 1464
	SCC { #39 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: x1
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #39
Number of SCCs: 13, DPs: 73, edges: 1463
	SCC { #10 #79 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #10 #79
Number of SCCs: 13, DPs: 71, edges: 1459
	SCC { #3 #28 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #3
Number of SCCs: 13, DPs: 70, edges: 1456
	SCC { #28 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #28
Number of SCCs: 12, DPs: 69, edges: 1455
	SCC { #95 #182 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: x1
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #95 #182
Number of SCCs: 12, DPs: 67, edges: 1451
	SCC { #23 #103 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #23 #103
Number of SCCs: 11, DPs: 65, edges: 1447
	SCC { #96 #131 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: x2
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #96
Number of SCCs: 11, DPs: 64, edges: 1444
	SCC { #131 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: x1
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #131
Number of SCCs: 10, DPs: 63, edges: 1443
	SCC { #104 #114 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: x2 + x3
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #114
Number of SCCs: 11, DPs: 62, edges: 1440
	SCC { #104 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: x1
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #104
Number of SCCs: 10, DPs: 61, edges: 1439
	SCC { #38 #80 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #80
Number of SCCs: 11, DPs: 60, edges: 1436
	SCC { #38 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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
   U13(x1)	weight: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #38
Number of SCCs: 10, DPs: 59, edges: 1435
	SCC { #29 #121 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: x1
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #29 #121
Number of SCCs: 10, DPs: 57, edges: 1431
	SCC { #45 #57 #94 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: x2
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #57 #94
Number of SCCs: 10, DPs: 55, edges: 1423
	SCC { #45 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: x1
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(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: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #45
Number of SCCs: 9, DPs: 54, edges: 1422
	SCC { #22 #44 #146 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 8) + x1
     0()	weight: 0
   #x(x1,x2)	weight: x1
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 8) + x1
   U32(x1,x2)	weight: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #22 #44
Number of SCCs: 10, DPs: 52, edges: 1414
	SCC { #146 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 8) + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: 0
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 8) + x1
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 8) + x1
     0()	weight: 0
   #x(x1,x2)	weight: x2
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 8) + x1
   U32(x1,x2)	weight: x2
   U33(x1)	weight: (/ 1 8)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1
   U61(x1)	weight: (/ 1 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 3 8) + x1
   U31(x1,x2,x3)	weight: x3
 #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: (/ 1 8)
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 1 8) + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #146
Number of SCCs: 9, DPs: 51, edges: 1413
	SCC { #5 #7 #9 #15 #18 #20 #41 #50 #90 #102 #118 #127 #135 #141 #145 #152 #157 #164 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 8) + x1
   U21(x1,x2)	weight: (/ 1 8) + x1 + x2
   U11(x1,x2,x3)	weight: (/ 1 8) + x1
     s(x1)	weight: (/ 1 4) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 3 8) + x1 + x2 + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x1
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: (/ 1 8) + x1
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 4) + x1 + x2
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 4)
    ok(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: (/ 1 8) + x1 + x2
   U33(x1)	weight: (/ 1 8) + x1
#proper(x1)	weight: 0
 isNat(x1)	weight: x1
  plus(x1,x2)	weight: (/ 1 4) + x1 + x2
   U61(x1)	weight: (/ 1 8) + 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 8) + x1 + x3
 #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: (/ 1 8) + x1
   U22(x1)	weight: (/ 1 8) + x1
   U51(x1,x2,x3)	weight: (/ 3 8) + x1 + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 8) + x1 + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #5 #7 #9 #15 #18 #20 #41 #50 #90 #102 #118 #127 #135 #141 #145 #152 #157 #164
Number of SCCs: 9, DPs: 33, edges: 1089
	SCC { #12 #25..27 #31 #34 #35 #37 #47 #48 #56 #63 #64 #74 #76..78 #82..84 #92 #93 #98..100 #124 #125 #129 #130 #133 #162 #180 #181 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U32(x1,x2)	weight: 0
isNatKind(x1)	weight: (/ 1 16) + x1
   U21(x1,x2)	weight: (/ 1 16) + x1 + x2
   U11(x1,x2,x3)	weight: (/ 1 16) + x1 + x2 + x3
     s(x1)	weight: (/ 7 32) + x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 16) + x1 + x2 + x3
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 16) + x1 + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
 #U13(x1)	weight: 0
   U12(x1,x2)	weight: (/ 1 16) + x1 + x2
 #U33(x1)	weight: 0
     x(x1,x2)	weight: (/ 7 32) + x1 + x2
 #U12(x1,x2)	weight: 0
proper(x1)	weight: (/ 1 8)
    ok(x1)	weight: (/ 1 16) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 16) + x1
   U32(x1,x2)	weight: (/ 1 16) + x1 + x2
   U33(x1)	weight: (/ 1 16) + x1
#proper(x1)	weight: x1
 isNat(x1)	weight: (/ 1 16) + x1
  plus(x1,x2)	weight: (/ 1 16) + x1 + x2
   U61(x1)	weight: (/ 1 16) + x1
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2,x3)	weight: 0
active(x1)	weight: (/ 9 32) + x1
   U31(x1,x2,x3)	weight: (/ 1 16) + x1 + x2 + x3
 #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: (/ 1 16) + x1
   U22(x1)	weight: (/ 1 16) + x1
   U51(x1,x2,x3)	weight: (/ 1 16) + x1 + x2 + x3
#isNatKind(x1)	weight: 0
   U41(x1,x2)	weight: (/ 1 16) + x1 + x2
 #U31(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #12 #25..27 #31 #34 #35 #37 #47 #48 #56 #63 #64 #74 #76..78 #82..84 #92 #93 #98..100 #124 #125 #129 #130 #133 #162 #180 #181
Number of SCCs: 8, DPs: 0, edges: 0
YES