Input TRS:
    1: U101(tt(),M,N) -> U102(isNatKind(activate(M)),activate(M),activate(N))
    2: U102(tt(),M,N) -> U103(isNat(activate(N)),activate(M),activate(N))
    3: U103(tt(),M,N) -> U104(isNatKind(activate(N)),activate(M),activate(N))
    4: U104(tt(),M,N) -> plus(x(activate(N),activate(M)),activate(N))
    5: U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
    6: U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
    7: U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
    8: U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
    9: U15(tt(),V2) -> U16(isNat(activate(V2)))
    10: U16(tt()) -> tt()
    11: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
    12: U22(tt(),V1) -> U23(isNat(activate(V1)))
    13: U23(tt()) -> tt()
    14: U31(tt(),V1,V2) -> U32(isNatKind(activate(V1)),activate(V1),activate(V2))
    15: U32(tt(),V1,V2) -> U33(isNatKind(activate(V2)),activate(V1),activate(V2))
    16: U33(tt(),V1,V2) -> U34(isNatKind(activate(V2)),activate(V1),activate(V2))
    17: U34(tt(),V1,V2) -> U35(isNat(activate(V1)),activate(V2))
    18: U35(tt(),V2) -> U36(isNat(activate(V2)))
    19: U36(tt()) -> tt()
    20: U41(tt(),V2) -> U42(isNatKind(activate(V2)))
    21: U42(tt()) -> tt()
    22: U51(tt()) -> tt()
    23: U61(tt(),V2) -> U62(isNatKind(activate(V2)))
    24: U62(tt()) -> tt()
    25: U71(tt(),N) -> U72(isNatKind(activate(N)),activate(N))
    26: U72(tt(),N) -> activate(N)
    27: U81(tt(),M,N) -> U82(isNatKind(activate(M)),activate(M),activate(N))
    28: U82(tt(),M,N) -> U83(isNat(activate(N)),activate(M),activate(N))
    29: U83(tt(),M,N) -> U84(isNatKind(activate(N)),activate(M),activate(N))
    30: U84(tt(),M,N) -> s(plus(activate(N),activate(M)))
    31: U91(tt(),N) -> U92(isNatKind(activate(N)))
    32: U92(tt()) -> |0|()
    33: isNat(n__0()) -> tt()
    34: isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
    35: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
    36: isNat(n__x(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V1),activate(V2))
    37: isNatKind(n__0()) -> tt()
    38: isNatKind(n__plus(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V2))
    39: isNatKind(n__s(V1)) -> U51(isNatKind(activate(V1)))
    40: isNatKind(n__x(V1,V2)) -> U61(isNatKind(activate(V1)),activate(V2))
    41: plus(N,|0|()) -> U71(isNat(N),N)
    42: plus(N,s(M)) -> U81(isNat(M),M,N)
    43: x(N,|0|()) -> U91(isNat(N),N)
    44: x(N,s(M)) -> U101(isNat(M),M,N)
    45: |0|() -> n__0()
    46: plus(X1,X2) -> n__plus(X1,X2)
    47: s(X) -> n__s(X)
    48: x(X1,X2) -> n__x(X1,X2)
    49: activate(n__0()) -> |0|()
    50: activate(n__plus(X1,X2)) -> plus(activate(X1),activate(X2))
    51: activate(n__s(X)) -> s(activate(X))
    52: activate(n__x(X1,X2)) -> x(activate(X1),activate(X2))
    53: activate(X) -> X
Number of strict rules: 53
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #U102(tt(),M,N) -> #U103(isNat(activate(N)),activate(M),activate(N))
   #2: #U102(tt(),M,N) -> #isNat(activate(N))
   #3: #U102(tt(),M,N) -> #activate(N)
   #4: #U102(tt(),M,N) -> #activate(M)
   #5: #U102(tt(),M,N) -> #activate(N)
   #6: #x(N,|0|()) -> #U91(isNat(N),N)
   #7: #x(N,|0|()) -> #isNat(N)
   #8: #U83(tt(),M,N) -> #U84(isNatKind(activate(N)),activate(M),activate(N))
   #9: #U83(tt(),M,N) -> #isNatKind(activate(N))
   #10: #U83(tt(),M,N) -> #activate(N)
   #11: #U83(tt(),M,N) -> #activate(M)
   #12: #U83(tt(),M,N) -> #activate(N)
   #13: #isNat(n__s(V1)) -> #U21(isNatKind(activate(V1)),activate(V1))
   #14: #isNat(n__s(V1)) -> #isNatKind(activate(V1))
   #15: #isNat(n__s(V1)) -> #activate(V1)
   #16: #isNat(n__s(V1)) -> #activate(V1)
   #17: #plus(N,s(M)) -> #U81(isNat(M),M,N)
   #18: #plus(N,s(M)) -> #isNat(M)
   #19: #plus(N,|0|()) -> #U71(isNat(N),N)
   #20: #plus(N,|0|()) -> #isNat(N)
   #21: #isNatKind(n__plus(V1,V2)) -> #U41(isNatKind(activate(V1)),activate(V2))
   #22: #isNatKind(n__plus(V1,V2)) -> #isNatKind(activate(V1))
   #23: #isNatKind(n__plus(V1,V2)) -> #activate(V1)
   #24: #isNatKind(n__plus(V1,V2)) -> #activate(V2)
   #25: #U12(tt(),V1,V2) -> #U13(isNatKind(activate(V2)),activate(V1),activate(V2))
   #26: #U12(tt(),V1,V2) -> #isNatKind(activate(V2))
   #27: #U12(tt(),V1,V2) -> #activate(V2)
   #28: #U12(tt(),V1,V2) -> #activate(V1)
   #29: #U12(tt(),V1,V2) -> #activate(V2)
   #30: #isNatKind(n__x(V1,V2)) -> #U61(isNatKind(activate(V1)),activate(V2))
   #31: #isNatKind(n__x(V1,V2)) -> #isNatKind(activate(V1))
   #32: #isNatKind(n__x(V1,V2)) -> #activate(V1)
   #33: #isNatKind(n__x(V1,V2)) -> #activate(V2)
   #34: #activate(n__s(X)) -> #s(activate(X))
   #35: #activate(n__s(X)) -> #activate(X)
   #36: #U15(tt(),V2) -> #U16(isNat(activate(V2)))
   #37: #U15(tt(),V2) -> #isNat(activate(V2))
   #38: #U15(tt(),V2) -> #activate(V2)
   #39: #U21(tt(),V1) -> #U22(isNatKind(activate(V1)),activate(V1))
   #40: #U21(tt(),V1) -> #isNatKind(activate(V1))
   #41: #U21(tt(),V1) -> #activate(V1)
   #42: #U21(tt(),V1) -> #activate(V1)
   #43: #U61(tt(),V2) -> #U62(isNatKind(activate(V2)))
   #44: #U61(tt(),V2) -> #isNatKind(activate(V2))
   #45: #U61(tt(),V2) -> #activate(V2)
   #46: #U22(tt(),V1) -> #U23(isNat(activate(V1)))
   #47: #U22(tt(),V1) -> #isNat(activate(V1))
   #48: #U22(tt(),V1) -> #activate(V1)
   #49: #U91(tt(),N) -> #U92(isNatKind(activate(N)))
   #50: #U91(tt(),N) -> #isNatKind(activate(N))
   #51: #U91(tt(),N) -> #activate(N)
   #52: #U31(tt(),V1,V2) -> #U32(isNatKind(activate(V1)),activate(V1),activate(V2))
   #53: #U31(tt(),V1,V2) -> #isNatKind(activate(V1))
   #54: #U31(tt(),V1,V2) -> #activate(V1)
   #55: #U31(tt(),V1,V2) -> #activate(V1)
   #56: #U31(tt(),V1,V2) -> #activate(V2)
   #57: #U84(tt(),M,N) -> #s(plus(activate(N),activate(M)))
   #58: #U84(tt(),M,N) -> #plus(activate(N),activate(M))
   #59: #U84(tt(),M,N) -> #activate(N)
   #60: #U84(tt(),M,N) -> #activate(M)
   #61: #activate(n__x(X1,X2)) -> #x(activate(X1),activate(X2))
   #62: #activate(n__x(X1,X2)) -> #activate(X1)
   #63: #activate(n__x(X1,X2)) -> #activate(X2)
   #64: #activate(n__0()) -> #|0|()
   #65: #U71(tt(),N) -> #U72(isNatKind(activate(N)),activate(N))
   #66: #U71(tt(),N) -> #isNatKind(activate(N))
   #67: #U71(tt(),N) -> #activate(N)
   #68: #U71(tt(),N) -> #activate(N)
   #69: #U41(tt(),V2) -> #U42(isNatKind(activate(V2)))
   #70: #U41(tt(),V2) -> #isNatKind(activate(V2))
   #71: #U41(tt(),V2) -> #activate(V2)
   #72: #U13(tt(),V1,V2) -> #U14(isNatKind(activate(V2)),activate(V1),activate(V2))
   #73: #U13(tt(),V1,V2) -> #isNatKind(activate(V2))
   #74: #U13(tt(),V1,V2) -> #activate(V2)
   #75: #U13(tt(),V1,V2) -> #activate(V1)
   #76: #U13(tt(),V1,V2) -> #activate(V2)
   #77: #isNatKind(n__s(V1)) -> #U51(isNatKind(activate(V1)))
   #78: #isNatKind(n__s(V1)) -> #isNatKind(activate(V1))
   #79: #isNatKind(n__s(V1)) -> #activate(V1)
   #80: #U11(tt(),V1,V2) -> #U12(isNatKind(activate(V1)),activate(V1),activate(V2))
   #81: #U11(tt(),V1,V2) -> #isNatKind(activate(V1))
   #82: #U11(tt(),V1,V2) -> #activate(V1)
   #83: #U11(tt(),V1,V2) -> #activate(V1)
   #84: #U11(tt(),V1,V2) -> #activate(V2)
   #85: #x(N,s(M)) -> #U101(isNat(M),M,N)
   #86: #x(N,s(M)) -> #isNat(M)
   #87: #U82(tt(),M,N) -> #U83(isNat(activate(N)),activate(M),activate(N))
   #88: #U82(tt(),M,N) -> #isNat(activate(N))
   #89: #U82(tt(),M,N) -> #activate(N)
   #90: #U82(tt(),M,N) -> #activate(M)
   #91: #U82(tt(),M,N) -> #activate(N)
   #92: #isNat(n__plus(V1,V2)) -> #U11(isNatKind(activate(V1)),activate(V1),activate(V2))
   #93: #isNat(n__plus(V1,V2)) -> #isNatKind(activate(V1))
   #94: #isNat(n__plus(V1,V2)) -> #activate(V1)
   #95: #isNat(n__plus(V1,V2)) -> #activate(V1)
   #96: #isNat(n__plus(V1,V2)) -> #activate(V2)
   #97: #U81(tt(),M,N) -> #U82(isNatKind(activate(M)),activate(M),activate(N))
   #98: #U81(tt(),M,N) -> #isNatKind(activate(M))
   #99: #U81(tt(),M,N) -> #activate(M)
   #100: #U81(tt(),M,N) -> #activate(M)
   #101: #U81(tt(),M,N) -> #activate(N)
   #102: #U34(tt(),V1,V2) -> #U35(isNat(activate(V1)),activate(V2))
   #103: #U34(tt(),V1,V2) -> #isNat(activate(V1))
   #104: #U34(tt(),V1,V2) -> #activate(V1)
   #105: #U34(tt(),V1,V2) -> #activate(V2)
   #106: #U92(tt()) -> #|0|()
   #107: #U72(tt(),N) -> #activate(N)
   #108: #isNat(n__x(V1,V2)) -> #U31(isNatKind(activate(V1)),activate(V1),activate(V2))
   #109: #isNat(n__x(V1,V2)) -> #isNatKind(activate(V1))
   #110: #isNat(n__x(V1,V2)) -> #activate(V1)
   #111: #isNat(n__x(V1,V2)) -> #activate(V1)
   #112: #isNat(n__x(V1,V2)) -> #activate(V2)
   #113: #U33(tt(),V1,V2) -> #U34(isNatKind(activate(V2)),activate(V1),activate(V2))
   #114: #U33(tt(),V1,V2) -> #isNatKind(activate(V2))
   #115: #U33(tt(),V1,V2) -> #activate(V2)
   #116: #U33(tt(),V1,V2) -> #activate(V1)
   #117: #U33(tt(),V1,V2) -> #activate(V2)
   #118: #U103(tt(),M,N) -> #U104(isNatKind(activate(N)),activate(M),activate(N))
   #119: #U103(tt(),M,N) -> #isNatKind(activate(N))
   #120: #U103(tt(),M,N) -> #activate(N)
   #121: #U103(tt(),M,N) -> #activate(M)
   #122: #U103(tt(),M,N) -> #activate(N)
   #123: #U101(tt(),M,N) -> #U102(isNatKind(activate(M)),activate(M),activate(N))
   #124: #U101(tt(),M,N) -> #isNatKind(activate(M))
   #125: #U101(tt(),M,N) -> #activate(M)
   #126: #U101(tt(),M,N) -> #activate(M)
   #127: #U101(tt(),M,N) -> #activate(N)
   #128: #U14(tt(),V1,V2) -> #U15(isNat(activate(V1)),activate(V2))
   #129: #U14(tt(),V1,V2) -> #isNat(activate(V1))
   #130: #U14(tt(),V1,V2) -> #activate(V1)
   #131: #U14(tt(),V1,V2) -> #activate(V2)
   #132: #U32(tt(),V1,V2) -> #U33(isNatKind(activate(V2)),activate(V1),activate(V2))
   #133: #U32(tt(),V1,V2) -> #isNatKind(activate(V2))
   #134: #U32(tt(),V1,V2) -> #activate(V2)
   #135: #U32(tt(),V1,V2) -> #activate(V1)
   #136: #U32(tt(),V1,V2) -> #activate(V2)
   #137: #U104(tt(),M,N) -> #plus(x(activate(N),activate(M)),activate(N))
   #138: #U104(tt(),M,N) -> #x(activate(N),activate(M))
   #139: #U104(tt(),M,N) -> #activate(N)
   #140: #U104(tt(),M,N) -> #activate(M)
   #141: #U104(tt(),M,N) -> #activate(N)
   #142: #activate(n__plus(X1,X2)) -> #plus(activate(X1),activate(X2))
   #143: #activate(n__plus(X1,X2)) -> #activate(X1)
   #144: #activate(n__plus(X1,X2)) -> #activate(X2)
   #145: #U35(tt(),V2) -> #U36(isNat(activate(V2)))
   #146: #U35(tt(),V2) -> #isNat(activate(V2))
   #147: #U35(tt(),V2) -> #activate(V2)
Number of SCCs: 1, DPs: 136, edges: 999
	SCC { #1..33 #35 #37..42 #44 #45 #47 #48 #50..56 #58..63 #65..68 #70..76 #78..105 #107..144 #146 #147 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: (/ 1 4)
 #U72(x1,x2)	weight: max{0, x2}
 #U32(x1,x2,x3)	weight: max{0, x3, x2}
isNatKind(x1)	weight: x1
   U16(x1)	weight: (/ 1 2)
   U21(x1,x2)	weight: max{0, (/ 1 4) + x2}
 #U83(x1,x2,x3)	weight: max{0, x3, x2}
 #|0|()	weight: 0
   U11(x1,x2,x3)	weight: max{0, (/ 1 4) + x2}
     s(x1)	weight: x1
#isNat(x1)	weight: x1
   U42(x1)	weight: x1
   U91(x1,x2)	weight: max{0, (/ 1 4) + x2}
 #U35(x1,x2)	weight: max{0, x2}
#U101(x1,x2,x3)	weight: max{0, (/ 1 2) + x3, x2}
activate(x1)	weight: x1
 #U82(x1,x2,x3)	weight: max{0, x3, x2}
#U104(x1,x2,x3)	weight: max{0, (/ 1 2) + x3, x2}
   U71(x1,x2)	weight: max{0, x2}
 #U81(x1,x2,x3)	weight: max{0, x3, x2}
 #U92(x1)	weight: 0
#plus(x1,x2)	weight: max{x2, x1}
  U101(x1,x2,x3)	weight: max{0, (/ 1 2) + x3, x2}
#activate(x1)	weight: x1
  U103(x1,x2,x3)	weight: max{0, (/ 1 2) + x3, x2}
 #U23(x1)	weight: 0
   U84(x1,x2,x3)	weight: max{0, x3, (/ 1 2) + x2}
   U23(x1)	weight: x1
   U35(x1,x2)	weight: max{0, (/ 1 4) + x2}
   U72(x1,x2)	weight: max{0, x2}
 #U13(x1,x2,x3)	weight: max{0, x3, x2}
   U34(x1,x2,x3)	weight: max{0, (/ 1 4) + x3}
#U103(x1,x2,x3)	weight: max{(/ 1 2) + x3, x2, (/ 1 4) + x1}
   U12(x1,x2,x3)	weight: max{0, (/ 1 4) + x2}
 #U33(x1,x2,x3)	weight: max{0, x3, x2}
     x(x1,x2)	weight: max{x2, (/ 1 2) + x1}
 #U16(x1)	weight: 0
  n__s(x1)	weight: x1
  U104(x1,x2,x3)	weight: max{0, (/ 1 2) + x3, x2}
 #U42(x1)	weight: 0
 #U12(x1,x2,x3)	weight: max{0, x3, x2}
 #U62(x1)	weight: 0
   U83(x1,x2,x3)	weight: max{0, x3, (/ 1 2) + x2}
 #U14(x1,x2,x3)	weight: max{0, x3, x2}
 #U36(x1)	weight: 0
   U36(x1)	weight: x1
#U102(x1,x2,x3)	weight: max{0, (/ 1 2) + x3, x2}
   #x(x1,x2)	weight: max{x2, (/ 1 2) + x1}
   #s(x1)	weight: 0
   U62(x1)	weight: x1
n__plus(x1,x2)	weight: max{(/ 1 2) + x2, x1}
 #U15(x1,x2)	weight: max{0, x2}
   U32(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, x2}
   U33(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, x2}
  n__0()	weight: (/ 1 4)
 #U34(x1,x2,x3)	weight: max{0, x3, x2}
   U14(x1,x2,x3)	weight: max{0, (/ 1 4) + x2}
 isNat(x1)	weight: (/ 1 4) + x1
  n__x(x1,x2)	weight: max{x2, (/ 1 2) + x1}
  plus(x1,x2)	weight: max{(/ 1 2) + x2, x1}
   U15(x1,x2)	weight: max{0, x1}
   U61(x1,x2)	weight: max{0, x2}
 #U51(x1)	weight: 0
 #U11(x1,x2,x3)	weight: max{0, x3, x2}
   U31(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, x2}
   U92(x1)	weight: (/ 1 4)
 #U41(x1,x2)	weight: max{0, (/ 1 4) + x2}
  U102(x1,x2,x3)	weight: max{0, (/ 1 2) + x3, x2}
 #U21(x1,x2)	weight: max{0, x2}
   U81(x1,x2,x3)	weight: max{0, x3, (/ 1 2) + x2}
   U82(x1,x2,x3)	weight: max{0, x3, (/ 1 2) + x2}
 #U22(x1,x2)	weight: max{0, x2}
    tt()	weight: (/ 1 2)
 #U84(x1,x2,x3)	weight: max{0, x3, x2}
 #U71(x1,x2)	weight: max{0, x2}
   U13(x1,x2,x3)	weight: max{0, (/ 1 4) + x2}
   U22(x1,x2)	weight: max{0, (/ 1 4) + x2}
   U51(x1)	weight: x1
#isNatKind(x1)	weight: x1
   U41(x1,x2)	weight: max{0, (/ 3 4) + x2}
 #U31(x1,x2,x3)	weight: max{0, x3, x2}
 #U91(x1,x2)	weight: max{(/ 1 4) + x2, x1}
 #U61(x1,x2)	weight: max{0, x2}
    Usable rules: { 1..19 25..36 41..53 }
    Removed DPs: #2 #3 #5..7 #21 #24 #31 #32 #50 #51 #62 #70 #71 #96 #109..111 #119 #120 #122 #127 #139 #141 #144
Number of SCCs: 1, DPs: 111, edges: 576
	SCC { #1 #4 #8..20 #22 #23 #25..30 #33 #35 #37..42 #44 #45 #47 #48 #52..56 #58..61 #63 #65..68 #72..76 #78..95 #97..105 #107 #108 #112..118 #121 #123..126 #128..138 #140 #142 #143 #146 #147 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: (/ 1 16)
 #U72(x1,x2)	weight: max{0, x2}
 #U32(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 1 2) + x2}
isNatKind(x1)	weight: x1
   U16(x1)	weight: (/ 1 8)
   U21(x1,x2)	weight: max{0, (/ 3 16) + x1}
 #U83(x1,x2,x3)	weight: max{0, x3, x2}
 #|0|()	weight: 0
   U11(x1,x2,x3)	weight: max{0, (/ 1 16) + x2, (/ 3 16) + x1}
     s(x1)	weight: x1
#isNat(x1)	weight: x1
   U42(x1)	weight: x1
   U91(x1,x2)	weight: max{0, (/ 3 4) + x2}
 #U35(x1,x2)	weight: max{0, (/ 1 16) + x2}
#U101(x1,x2,x3)	weight: max{0, (/ 3 4) + x3, (/ 5 8) + x2}
activate(x1)	weight: x1
 #U82(x1,x2,x3)	weight: max{0, x3, x2}
#U104(x1,x2,x3)	weight: max{0, (/ 3 4) + x3, (/ 5 8) + x2}
   U71(x1,x2)	weight: max{0, x2}
 #U81(x1,x2,x3)	weight: max{0, x3, x2}
 #U92(x1)	weight: 0
#plus(x1,x2)	weight: max{x2, x1}
  U101(x1,x2,x3)	weight: max{0, (/ 3 4) + x3, (/ 5 8) + x2}
#activate(x1)	weight: x1
  U103(x1,x2,x3)	weight: max{0, (/ 3 4) + x3, (/ 5 8) + x2}
 #U23(x1)	weight: 0
   U84(x1,x2,x3)	weight: max{0, x3, x2}
   U23(x1)	weight: (/ 1 16)
   U35(x1,x2)	weight: max{0, x1}
   U72(x1,x2)	weight: max{0, x2}
 #U13(x1,x2,x3)	weight: max{0, x3, x2}
   U34(x1,x2,x3)	weight: max{0, (/ 5 16) + x3, (/ 5 16) + x1}
#U103(x1,x2,x3)	weight: max{0, (/ 3 4) + x3, (/ 5 8) + x2}
   U12(x1,x2,x3)	weight: max{0, (/ 7 16) + x3}
 #U33(x1,x2,x3)	weight: max{0, (/ 3 16) + x3, (/ 5 16) + x2}
     x(x1,x2)	weight: max{(/ 5 8) + x2, (/ 3 4) + x1}
 #U16(x1)	weight: 0
  n__s(x1)	weight: x1
  U104(x1,x2,x3)	weight: max{0, (/ 3 4) + x3, (/ 5 8) + x2}
 #U42(x1)	weight: 0
 #U12(x1,x2,x3)	weight: max{0, x3, x2}
 #U62(x1)	weight: 0
   U83(x1,x2,x3)	weight: max{0, x3, x2}
 #U14(x1,x2,x3)	weight: max{0, x3, x2}
 #U36(x1)	weight: 0
   U36(x1)	weight: (/ 1 8) + x1
#U102(x1,x2,x3)	weight: max{0, (/ 3 4) + x3, (/ 5 8) + x2}
   #x(x1,x2)	weight: max{(/ 5 8) + x2, (/ 3 4) + x1}
   #s(x1)	weight: 0
   U62(x1)	weight: x1
n__plus(x1,x2)	weight: max{x2, x1}
 #U15(x1,x2)	weight: max{0, x2}
   U32(x1,x2,x3)	weight: max{0, x1}
   U33(x1,x2,x3)	weight: max{0, x3, (/ 1 4) + x2}
  n__0()	weight: (/ 1 16)
 #U34(x1,x2,x3)	weight: max{0, (/ 1 8) + x3, (/ 1 4) + x2}
   U14(x1,x2,x3)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  n__x(x1,x2)	weight: max{(/ 5 8) + x2, (/ 3 4) + x1}
  plus(x1,x2)	weight: max{x2, x1}
   U15(x1,x2)	weight: max{(/ 1 16) + x2, x1}
   U61(x1,x2)	weight: 0
 #U51(x1)	weight: 0
 #U11(x1,x2,x3)	weight: max{0, x3, x2}
   U31(x1,x2,x3)	weight: max{0, (/ 1 16) + x1}
   U92(x1)	weight: (/ 1 16)
 #U41(x1,x2)	weight: 0
  U102(x1,x2,x3)	weight: max{0, (/ 3 4) + x3, (/ 5 8) + x2}
 #U21(x1,x2)	weight: max{0, x2}
   U81(x1,x2,x3)	weight: max{0, x3, x2}
   U82(x1,x2,x3)	weight: max{0, x3, x2}
 #U22(x1,x2)	weight: max{0, x2}
    tt()	weight: (/ 3 16)
 #U84(x1,x2,x3)	weight: max{0, x3, x2}
 #U71(x1,x2)	weight: max{0, x2}
   U13(x1,x2,x3)	weight: max{0, (/ 1 2) + x2}
   U22(x1,x2)	weight: 0
   U51(x1)	weight: x1
#isNatKind(x1)	weight: x1
   U41(x1,x2)	weight: max{0, (/ 1 16) + x2}
 #U31(x1,x2,x3)	weight: max{0, (/ 7 16) + x3, (/ 9 16) + x2}
 #U91(x1,x2)	weight: 0
 #U61(x1,x2)	weight: max{0, (/ 1 16) + x2}
    Usable rules: { 1..4 25..32 41..53 }
    Removed DPs: #4 #30 #33 #44 #45 #52..56 #63 #86 #102..105 #108 #112..117 #121 #124..126 #132..136 #140 #146 #147
Number of SCCs: 1, DPs: 76, edges: 309
	SCC { #1 #8..20 #22 #23 #25..29 #35 #37..42 #47 #48 #58..61 #65..68 #72..76 #78..85 #87..95 #97..101 #107 #118 #123 #128..131 #137 #138 #142 #143 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: (/ 1 16)
 #U72(x1,x2)	weight: max{0, (/ 1 16) + x2}
 #U32(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 1 2) + x2}
isNatKind(x1)	weight: x1
   U16(x1)	weight: (/ 1 8)
   U21(x1,x2)	weight: max{0, (/ 3 16) + x1}
 #U83(x1,x2,x3)	weight: max{0, (/ 1 16) + x3, (/ 1 8) + x2}
 #|0|()	weight: 0
   U11(x1,x2,x3)	weight: max{0, (/ 1 16) + x2, (/ 5 16) + x1}
     s(x1)	weight: x1
#isNat(x1)	weight: (/ 1 16) + x1
   U42(x1)	weight: x1
   U91(x1,x2)	weight: max{0, (/ 1 4) + x2}
 #U35(x1,x2)	weight: max{0, (/ 1 16) + x2}
#U101(x1,x2,x3)	weight: max{0, (/ 5 16) + x3, (/ 3 16) + x2}
activate(x1)	weight: x1
 #U82(x1,x2,x3)	weight: max{0, (/ 1 16) + x3, (/ 1 8) + x2}
#U104(x1,x2,x3)	weight: max{0, (/ 5 16) + x3, (/ 3 16) + x2}
   U71(x1,x2)	weight: max{0, x2}
 #U81(x1,x2,x3)	weight: max{0, (/ 1 16) + x3, (/ 1 8) + x2}
 #U92(x1)	weight: 0
#plus(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 16) + x1}
  U101(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, (/ 1 8) + x2}
#activate(x1)	weight: (/ 1 16) + x1
  U103(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, (/ 1 8) + x2}
 #U23(x1)	weight: 0
   U84(x1,x2,x3)	weight: max{0, x3, (/ 1 8) + x2}
   U23(x1)	weight: (/ 1 16)
   U35(x1,x2)	weight: max{0, x1}
   U72(x1,x2)	weight: max{0, x2}
 #U13(x1,x2,x3)	weight: max{0, (/ 1 16) + x3, (/ 1 16) + x2}
   U34(x1,x2,x3)	weight: max{0, (/ 5 16) + x3, (/ 5 16) + x1}
#U103(x1,x2,x3)	weight: max{0, (/ 5 16) + x3, (/ 3 16) + x2}
   U12(x1,x2,x3)	weight: max{0, (/ 9 16) + x3}
 #U33(x1,x2,x3)	weight: max{0, (/ 3 16) + x3, (/ 5 16) + x2}
     x(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 4) + x1}
 #U16(x1)	weight: 0
  n__s(x1)	weight: x1
  U104(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, (/ 1 8) + x2}
 #U42(x1)	weight: 0
 #U12(x1,x2,x3)	weight: max{0, (/ 1 16) + x3, (/ 1 16) + x2}
 #U62(x1)	weight: 0
   U83(x1,x2,x3)	weight: max{0, x3, (/ 1 8) + x2}
 #U14(x1,x2,x3)	weight: max{0, (/ 1 16) + x3, (/ 1 16) + x2}
 #U36(x1)	weight: 0
   U36(x1)	weight: (/ 1 8) + x1
#U102(x1,x2,x3)	weight: max{0, (/ 5 16) + x3, (/ 3 16) + x2}
   #x(x1,x2)	weight: max{(/ 3 16) + x2, (/ 5 16) + x1}
   #s(x1)	weight: 0
   U62(x1)	weight: x1
n__plus(x1,x2)	weight: max{(/ 1 8) + x2, x1}
 #U15(x1,x2)	weight: max{0, (/ 1 16) + x2}
   U32(x1,x2,x3)	weight: max{0, x1}
   U33(x1,x2,x3)	weight: max{0, x3, (/ 1 4) + x2}
  n__0()	weight: (/ 1 16)
 #U34(x1,x2,x3)	weight: max{0, (/ 1 8) + x3, (/ 1 4) + x2}
   U14(x1,x2,x3)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  n__x(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 4) + x1}
  plus(x1,x2)	weight: max{(/ 1 8) + x2, x1}
   U15(x1,x2)	weight: max{(/ 1 16) + x2, x1}
   U61(x1,x2)	weight: 0
 #U51(x1)	weight: 0
 #U11(x1,x2,x3)	weight: max{0, (/ 1 16) + x3, (/ 1 16) + x2}
   U31(x1,x2,x3)	weight: max{0, (/ 1 16) + x1}
   U92(x1)	weight: (/ 1 16)
 #U41(x1,x2)	weight: 0
  U102(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, (/ 1 8) + x2}
 #U21(x1,x2)	weight: max{0, (/ 1 16) + x2}
   U81(x1,x2,x3)	weight: max{0, x3, (/ 1 8) + x2}
   U82(x1,x2,x3)	weight: max{0, x3, (/ 1 8) + x2}
 #U22(x1,x2)	weight: max{0, (/ 1 16) + x2}
    tt()	weight: (/ 3 16)
 #U84(x1,x2,x3)	weight: max{0, (/ 1 16) + x3, (/ 1 8) + x2}
 #U71(x1,x2)	weight: max{0, (/ 1 16) + x2}
   U13(x1,x2,x3)	weight: max{0, (/ 5 8) + x2}
   U22(x1,x2)	weight: 0
   U51(x1)	weight: x1
#isNatKind(x1)	weight: (/ 1 16) + x1
   U41(x1,x2)	weight: max{0, (/ 3 16) + x2}
 #U31(x1,x2,x3)	weight: max{0, (/ 7 16) + x3, (/ 9 16) + x2}
 #U91(x1,x2)	weight: 0
 #U61(x1,x2)	weight: max{0, (/ 1 16) + x2}
    Usable rules: { 1..4 25..32 41..53 }
    Removed DPs: #11 #18 #60 #90 #98..100
Number of SCCs: 1, DPs: 69, edges: 268
	SCC { #1 #8..10 #12..17 #19 #20 #22 #23 #25..29 #35 #37..42 #47 #48 #58 #59 #61 #65..68 #72..76 #78..85 #87..89 #91..95 #97 #101 #107 #118 #123 #128..131 #137 #138 #142 #143 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: (/ 1 16)
 #U72(x1,x2)	weight: max{0, (/ 3 16) + x2}
 #U32(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 1 2) + x2}
isNatKind(x1)	weight: x1
   U16(x1)	weight: (/ 1 8)
   U21(x1,x2)	weight: max{0, (/ 3 16) + x1}
 #U83(x1,x2,x3)	weight: max{0, (/ 3 16) + x3, (/ 1 16) + x2}
 #|0|()	weight: 0
   U11(x1,x2,x3)	weight: max{0, (/ 1 16) + x2, (/ 7 16) + x1}
     s(x1)	weight: x1
#isNat(x1)	weight: (/ 3 16) + x1
   U42(x1)	weight: x1
   U91(x1,x2)	weight: max{0, (/ 3 8) + x2}
 #U35(x1,x2)	weight: max{0, (/ 1 16) + x2}
#U101(x1,x2,x3)	weight: max{0, (/ 9 16) + x3, (/ 7 16) + x2}
activate(x1)	weight: x1
 #U82(x1,x2,x3)	weight: max{0, (/ 3 16) + x3, (/ 1 16) + x2}
#U104(x1,x2,x3)	weight: max{0, (/ 9 16) + x3, (/ 7 16) + x2}
   U71(x1,x2)	weight: max{0, x2}
 #U81(x1,x2,x3)	weight: max{0, (/ 3 16) + x3, (/ 1 16) + x2}
 #U92(x1)	weight: 0
#plus(x1,x2)	weight: max{(/ 1 16) + x2, (/ 3 16) + x1}
  U101(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 1 4) + x2}
#activate(x1)	weight: (/ 3 16) + x1
  U103(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 1 4) + x2}
 #U23(x1)	weight: 0
   U84(x1,x2,x3)	weight: max{0, x3, (/ 1 4) + x2}
   U23(x1)	weight: (/ 1 16)
   U35(x1,x2)	weight: max{0, x1}
   U72(x1,x2)	weight: max{0, x2}
 #U13(x1,x2,x3)	weight: max{0, (/ 5 16) + x3, (/ 3 16) + x2}
   U34(x1,x2,x3)	weight: max{0, (/ 5 16) + x3, (/ 5 16) + x1}
#U103(x1,x2,x3)	weight: max{0, (/ 9 16) + x3, (/ 7 16) + x2}
   U12(x1,x2,x3)	weight: max{0, (/ 11 16) + x3}
 #U33(x1,x2,x3)	weight: max{0, (/ 3 16) + x3, (/ 5 16) + x2}
     x(x1,x2)	weight: max{(/ 1 4) + x2, (/ 3 8) + x1}
 #U16(x1)	weight: 0
  n__s(x1)	weight: x1
  U104(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 1 4) + x2}
 #U42(x1)	weight: 0
 #U12(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 3 16) + x2}
 #U62(x1)	weight: 0
   U83(x1,x2,x3)	weight: max{0, x3, (/ 1 4) + x2}
 #U14(x1,x2,x3)	weight: max{0, (/ 5 16) + x3, (/ 3 16) + x2}
 #U36(x1)	weight: 0
   U36(x1)	weight: (/ 1 8) + x1
#U102(x1,x2,x3)	weight: max{0, (/ 9 16) + x3, (/ 7 16) + x2}
   #x(x1,x2)	weight: max{(/ 7 16) + x2, (/ 9 16) + x1}
   #s(x1)	weight: 0
   U62(x1)	weight: x1
n__plus(x1,x2)	weight: max{(/ 1 4) + x2, x1}
 #U15(x1,x2)	weight: max{0, (/ 1 4) + x2}
   U32(x1,x2,x3)	weight: max{0, x1}
   U33(x1,x2,x3)	weight: max{0, x3, (/ 1 4) + x2}
  n__0()	weight: (/ 1 16)
 #U34(x1,x2,x3)	weight: max{0, (/ 1 8) + x3, (/ 1 4) + x2}
   U14(x1,x2,x3)	weight: 0
 isNat(x1)	weight: (/ 1 8) + x1
  n__x(x1,x2)	weight: max{(/ 1 4) + x2, (/ 3 8) + x1}
  plus(x1,x2)	weight: max{(/ 1 4) + x2, x1}
   U15(x1,x2)	weight: max{(/ 1 16) + x2, x1}
   U61(x1,x2)	weight: 0
 #U51(x1)	weight: 0
 #U11(x1,x2,x3)	weight: max{0, (/ 7 16) + x3, (/ 3 16) + x2}
   U31(x1,x2,x3)	weight: max{0, (/ 1 16) + x1}
   U92(x1)	weight: (/ 1 16)
 #U41(x1,x2)	weight: 0
  U102(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 1 4) + x2}
 #U21(x1,x2)	weight: max{0, (/ 3 16) + x2}
   U81(x1,x2,x3)	weight: max{0, x3, (/ 1 4) + x2}
   U82(x1,x2,x3)	weight: max{0, x3, (/ 1 4) + x2}
 #U22(x1,x2)	weight: max{0, (/ 3 16) + x2}
    tt()	weight: (/ 3 16)
 #U84(x1,x2,x3)	weight: max{0, (/ 3 16) + x3, (/ 1 16) + x2}
 #U71(x1,x2)	weight: max{0, (/ 3 16) + x2}
   U13(x1,x2,x3)	weight: max{0, (/ 3 4) + x2}
   U22(x1,x2)	weight: 0
   U51(x1)	weight: x1
#isNatKind(x1)	weight: (/ 3 16) + x1
   U41(x1,x2)	weight: max{0, (/ 5 16) + x2}
 #U31(x1,x2,x3)	weight: max{0, (/ 7 16) + x3, (/ 9 16) + x2}
 #U91(x1,x2)	weight: 0
 #U61(x1,x2)	weight: max{0, (/ 1 16) + x2}
    Usable rules: { 1..4 25..32 41..53 }
    Removed DPs: #26 #27 #29 #37 #38 #73 #74 #76 #84 #128 #131
Number of SCCs: 1, DPs: 58, edges: 213
	SCC { #1 #8..10 #12..17 #19 #20 #22 #23 #25 #28 #35 #39..42 #47 #48 #58 #59 #61 #65..68 #72 #75 #78..83 #85 #87..89 #91..95 #97 #101 #107 #118 #123 #129 #130 #137 #138 #142 #143 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
   |0|()	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U91 U23 U72 #U13 U12 #U12 U32 n__0 isNat U15 U61 #U11 U31 U92 tt U13 U51
 #U72(x1,x2)	status: x2
 #U32(x1,x2,x3)	status: [x1]	precedence above:
isNatKind(x1)	status: []	precedence above: #U72 U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 tt U13 U51
   U16(x1)	status: []	precedence above: #U72 isNatKind U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 tt U13 U51
   U21(x1,x2)	status: []	precedence above: #U72 isNatKind U16 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 tt U13 U51
 #U83(x1,x2,x3)	status: [x3]	precedence above: #isNat #U82 #U81 #plus U72 #U13 #U12 #U14 #U11 #U84
 #|0|()	status: []	precedence above:
   U11(x1,x2,x3)	status: x1
     s(x1)	status: [x1]	precedence above: |0| #U72 isNatKind U16 U21 #isNat U91 U71 U23 U72 #U13 U12 n__s #U12 #U14 U32 n__0 U14 isNat U15 U61 #U11 U31 U92 #U21 #U22 tt U13 U51
#isNat(x1)	status: x1
   U42(x1)	status: x1
   U91(x1,x2)	status: []	precedence above: |0| #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 n__0 isNat U15 U61 #U11 U31 U92 tt U13 U51
 #U35(x1,x2)	status: []	precedence above:
#U101(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U82 #U104 U71 #U81 #plus U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt #U84 U13 U51
activate(x1)	status: x1
 #U82(x1,x2,x3)	status: [x3]	precedence above: #U83 #isNat #U81 #plus U72 #U13 #U12 #U14 #U11 #U84
#U104(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U101 #U82 U71 #U81 #plus U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt #U84 U13 U51
   U71(x1,x2)	status: [x2]	precedence above: U72
 #U81(x1,x2,x3)	status: [x3]	precedence above: #U83 #isNat #U82 #plus U72 #U13 #U12 #U14 #U11 #U84
 #U92(x1)	status: []	precedence above:
#plus(x1,x2)	status: [x1]	precedence above: #U83 #isNat #U82 #U81 U72 #U13 #U12 #U14 #U11 #U84
  U101(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U101 #U82 #U104 U71 #U81 #plus U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt #U84 U13 U51
#activate(x1)	status: x1
  U103(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U101 #U82 #U104 U71 #U81 #plus U101 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt #U84 U13 U51
 #U23(x1)	status: []	precedence above:
   U84(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U82 U71 #U81 #plus U23 U72 #U13 U12 n__s #U12 U83 #U14 n__plus U32 n__0 U14 isNat plus U15 U61 #U11 U31 U92 #U21 U81 U82 #U22 tt #U84 U13 U51
   U23(x1)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 tt U13 U51
   U35(x1,x2)	status: x1
   U72(x1,x2)	status: [x2]	precedence above:
 #U13(x1,x2,x3)	status: x2
   U34(x1,x2,x3)	status: x1
#U103(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U101 #U82 #U104 U71 #U81 #plus U101 U103 U84 U23 U72 #U13 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt #U84 U13 U51
   U12(x1,x2,x3)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 #U12 U32 isNat U15 U61 #U11 U31 tt U13 U51
 #U33(x1,x2,x3)	status: [x2]	precedence above:
     x(x1,x2)	status: [x2,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U101 #U82 #U104 U71 #U81 #plus U101 U103 U84 U23 U72 #U13 #U103 U12 n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt #U84 U13 U51
 #U16(x1)	status: []	precedence above:
  n__s(x1)	status: [x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 U71 U23 U72 #U13 U12 #U12 #U14 U32 n__0 U14 isNat U15 U61 #U11 U31 U92 #U21 #U22 tt U13 U51
  U104(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U101 #U82 #U104 U71 #U81 #plus U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt #U84 U13 U51
 #U42(x1)	status: []	precedence above:
 #U12(x1,x2,x3)	status: x2
 #U62(x1)	status: []	precedence above:
   U83(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U82 U71 #U81 #plus U84 U23 U72 #U13 U12 n__s #U12 #U14 n__plus U32 n__0 U14 isNat plus U15 U61 #U11 U31 U92 #U21 U81 U82 #U22 tt #U84 U13 U51
 #U14(x1,x2,x3)	status: x2
 #U36(x1)	status: []	precedence above:
   U36(x1)	status: x1
#U102(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U101 #U82 #U104 U71 #U81 #plus U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt #U84 U13 U51
   #x(x1,x2)	status: [x2,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U101 #U82 #U104 U71 #U81 #plus U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt #U84 U13 U51
   #s(x1)	status: []	precedence above:
   U62(x1)	status: x1
n__plus(x1,x2)	status: [x2,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U82 U71 #U81 #plus U84 U23 U72 #U13 U12 n__s #U12 U83 #U14 U32 n__0 U14 isNat plus U15 U61 #U11 U31 U92 #U21 U81 U82 #U22 tt #U84 U13 U51
 #U15(x1,x2)	status: [x2,x1]	precedence above:
   U32(x1,x2,x3)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 isNat U15 U61 #U11 U31 tt U13 U51
   U33(x1,x2,x3)	status: x1
  n__0()	status: []	precedence above: |0| #U72 isNatKind U16 U21 #isNat U91 U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 U92 tt U13 U51
 #U34(x1,x2,x3)	status: [x2]	precedence above:
   U14(x1,x2,x3)	status: x1
 isNat(x1)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 U15 U61 #U11 U31 tt U13 U51
  n__x(x1,x2)	status: [x2,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U101 #U82 #U104 U71 #U81 #plus U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt #U84 U13 U51
  plus(x1,x2)	status: [x2,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U82 U71 #U81 #plus U84 U23 U72 #U13 U12 n__s #U12 U83 #U14 n__plus U32 n__0 U14 isNat U15 U61 #U11 U31 U92 #U21 U81 U82 #U22 tt #U84 U13 U51
   U15(x1,x2)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U61 #U11 U31 tt U13 U51
   U61(x1,x2)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 #U11 U31 tt U13 U51
 #U51(x1)	status: []	precedence above:
 #U11(x1,x2,x3)	status: x2
   U31(x1,x2,x3)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 tt U13 U51
   U92(x1)	status: []	precedence above: |0| #U72 isNatKind U16 U21 #isNat U91 U23 U72 #U13 U12 #U12 U32 n__0 isNat U15 U61 #U11 U31 tt U13 U51
 #U41(x1,x2)	status: [x2,x1]	precedence above:
  U102(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U101 #U82 #U104 U71 #U81 #plus U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 #U21 U81 U82 #U22 tt #U84 U13 U51
 #U21(x1,x2)	status: [x2]	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 #U14 U32 U14 isNat U15 U61 #U11 U31 #U22 tt U13 U51
   U81(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U82 U71 #U81 #plus U84 U23 U72 #U13 U12 n__s #U12 U83 #U14 n__plus U32 n__0 U14 isNat plus U15 U61 #U11 U31 U92 #U21 U82 #U22 tt #U84 U13 U51
   U82(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 #U83 s #isNat U91 #U82 U71 #U81 #plus U84 U23 U72 #U13 U12 n__s #U12 U83 #U14 n__plus U32 n__0 U14 isNat plus U15 U61 #U11 U31 U92 #U21 U81 #U22 tt #U84 U13 U51
 #U22(x1,x2)	status: [x2]	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 #U14 U32 U14 isNat U15 U61 #U11 U31 #U21 tt U13 U51
    tt()	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 U13 U51
 #U84(x1,x2,x3)	status: [x3]	precedence above: #U83 #isNat #U82 #U81 #plus U72 #U13 #U12 #U14 #U11
 #U71(x1,x2)	status: x2
   U13(x1,x2,x3)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 tt U51
   U22(x1,x2)	status: x1
   U51(x1)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 tt U13
#isNatKind(x1)	status: x1
   U41(x1,x2)	status: x1
 #U31(x1,x2,x3)	status: [x3,x1,x2]	precedence above:
 #U91(x1,x2)	status: []	precedence above:
 #U61(x1,x2)	status: []	precedence above:
    Usable rules: { 1..53 }
    Removed DPs: #9 #10 #12..16 #19 #20 #22 #23 #35 #40..42 #47 #48 #59 #78 #79 #85 #88 #89 #91..95 #101 #137 #138 #142 #143
Number of SCCs: 1, DPs: 5, edges: 5
	SCC { #8 #17 #58 #87 #97 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
   |0|()	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U91 U23 U72 #U13 U12 #U12 U32 n__0 isNat U15 U61 #U11 U31 U92 tt U13 U51
 #U72(x1,x2)	status: x2
 #U32(x1,x2,x3)	status: [x1]	precedence above:
isNatKind(x1)	status: []	precedence above: #U72 U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 tt U13 U51
   U16(x1)	status: []	precedence above: #U72 isNatKind U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 tt U13 U51
   U21(x1,x2)	status: []	precedence above: #U72 isNatKind U16 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 tt U13 U51
 #U83(x1,x2,x3)	status: [x3,x2]	precedence above: #isNat #U82 #U81 #plus U72 #U13 #U12 #U14 #U11 #U84
 #|0|()	status: []	precedence above:
   U11(x1,x2,x3)	status: x1
     s(x1)	status: [x1]	precedence above: |0| #U72 isNatKind U16 U21 #isNat U91 U71 U23 U72 #U13 U12 n__s #U12 #U14 U32 n__0 U14 isNat U15 U61 #U11 U31 U92 #U21 #U22 tt U13 U51
#isNat(x1)	status: x1
   U42(x1)	status: x1
   U91(x1,x2)	status: []	precedence above: |0| #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 n__0 isNat U15 U61 #U11 U31 U92 tt U13 U51
 #U35(x1,x2)	status: []	precedence above:
#U101(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 #U104 U71 U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt U13 U51
activate(x1)	status: x1
 #U82(x1,x2,x3)	status: [x3,x2]	precedence above: #U83 #isNat #U81 #plus U72 #U13 #U12 #U14 #U11 #U84
#U104(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 #U101 U71 U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt U13 U51
   U71(x1,x2)	status: [x2]	precedence above: U72
 #U81(x1,x2,x3)	status: [x3,x2,x1]	precedence above: #U83 #isNat #U82 #plus U72 #U13 #U12 #U14 #U11 #U84
 #U92(x1)	status: []	precedence above:
#plus(x1,x2)	status: [x1,x2]	precedence above: #U83 #isNat #U82 #U81 U72 #U13 #U12 #U14 #U11 #U84
  U101(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 #U101 #U104 U71 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt U13 U51
#activate(x1)	status: x1
  U103(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 #U101 #U104 U71 U101 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt U13 U51
 #U23(x1)	status: []	precedence above:
   U84(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 U71 U23 U72 #U13 U12 n__s #U12 U83 #U14 n__plus U32 n__0 U14 isNat plus U15 U61 #U11 U31 U92 #U21 U81 U82 #U22 tt U13 U51
   U23(x1)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 tt U13 U51
   U35(x1,x2)	status: x1
   U72(x1,x2)	status: [x2]	precedence above:
 #U13(x1,x2,x3)	status: x2
   U34(x1,x2,x3)	status: x1
#U103(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 #U101 #U104 U71 U101 U103 U84 U23 U72 #U13 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt U13 U51
   U12(x1,x2,x3)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 #U12 U32 isNat U15 U61 #U11 U31 tt U13 U51
 #U33(x1,x2,x3)	status: [x2]	precedence above:
     x(x1,x2)	status: [x2,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 #U101 #U104 U71 U101 U103 U84 U23 U72 #U13 #U103 U12 n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt U13 U51
 #U16(x1)	status: []	precedence above:
  n__s(x1)	status: [x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 U71 U23 U72 #U13 U12 #U12 #U14 U32 n__0 U14 isNat U15 U61 #U11 U31 U92 #U21 #U22 tt U13 U51
  U104(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 #U101 #U104 U71 U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt U13 U51
 #U42(x1)	status: []	precedence above:
 #U12(x1,x2,x3)	status: x2
 #U62(x1)	status: []	precedence above:
   U83(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 U71 U84 U23 U72 #U13 U12 n__s #U12 #U14 n__plus U32 n__0 U14 isNat plus U15 U61 #U11 U31 U92 #U21 U81 U82 #U22 tt U13 U51
 #U14(x1,x2,x3)	status: x2
 #U36(x1)	status: []	precedence above:
   U36(x1)	status: x1
#U102(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 #U101 #U104 U71 U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt U13 U51
   #x(x1,x2)	status: [x2,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 #U101 #U104 U71 U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt U13 U51
   #s(x1)	status: []	precedence above:
   U62(x1)	status: x1
n__plus(x1,x2)	status: [x2,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 U71 U84 U23 U72 #U13 U12 n__s #U12 U83 #U14 U32 n__0 U14 isNat plus U15 U61 #U11 U31 U92 #U21 U81 U82 #U22 tt U13 U51
 #U15(x1,x2)	status: [x2,x1]	precedence above:
   U32(x1,x2,x3)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 isNat U15 U61 #U11 U31 tt U13 U51
   U33(x1,x2,x3)	status: x1
  n__0()	status: []	precedence above: |0| #U72 isNatKind U16 U21 #isNat U91 U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 U92 tt U13 U51
 #U34(x1,x2,x3)	status: [x2]	precedence above:
   U14(x1,x2,x3)	status: x1
 isNat(x1)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 U15 U61 #U11 U31 tt U13 U51
  n__x(x1,x2)	status: [x2,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 #U101 #U104 U71 U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat plus U15 U61 #U11 U31 U92 U102 #U21 U81 U82 #U22 tt U13 U51
  plus(x1,x2)	status: [x2,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 U71 U84 U23 U72 #U13 U12 n__s #U12 U83 #U14 n__plus U32 n__0 U14 isNat U15 U61 #U11 U31 U92 #U21 U81 U82 #U22 tt U13 U51
   U15(x1,x2)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U61 #U11 U31 tt U13 U51
   U61(x1,x2)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 #U11 U31 tt U13 U51
 #U51(x1)	status: []	precedence above:
 #U11(x1,x2,x3)	status: x2
   U31(x1,x2,x3)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 tt U13 U51
   U92(x1)	status: []	precedence above: |0| #U72 isNatKind U16 U21 #isNat U91 U23 U72 #U13 U12 #U12 U32 n__0 isNat U15 U61 #U11 U31 tt U13 U51
 #U41(x1,x2)	status: [x2,x1]	precedence above:
  U102(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 #U101 #U104 U71 U101 U103 U84 U23 U72 #U13 #U103 U12 x n__s U104 #U12 U83 #U14 #U102 #x n__plus U32 n__0 U14 isNat n__x plus U15 U61 #U11 U31 U92 #U21 U81 U82 #U22 tt U13 U51
 #U21(x1,x2)	status: [x2]	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 #U14 U32 U14 isNat U15 U61 #U11 U31 #U22 tt U13 U51
   U81(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 U71 U84 U23 U72 #U13 U12 n__s #U12 U83 #U14 n__plus U32 n__0 U14 isNat plus U15 U61 #U11 U31 U92 #U21 U82 #U22 tt U13 U51
   U82(x1,x2,x3)	status: [x2,x3,x1]	precedence above: |0| #U72 isNatKind U16 U21 s #isNat U91 U71 U84 U23 U72 #U13 U12 n__s #U12 U83 #U14 n__plus U32 n__0 U14 isNat plus U15 U61 #U11 U31 U92 #U21 U81 #U22 tt U13 U51
 #U22(x1,x2)	status: [x2]	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 #U14 U32 U14 isNat U15 U61 #U11 U31 #U21 tt U13 U51
    tt()	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 U13 U51
 #U84(x1,x2,x3)	status: [x3,x2]	precedence above: #U83 #isNat #U82 #U81 #plus U72 #U13 #U12 #U14 #U11
 #U71(x1,x2)	status: x2
   U13(x1,x2,x3)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 tt U51
   U22(x1,x2)	status: x1
   U51(x1)	status: []	precedence above: #U72 isNatKind U16 U21 #isNat U23 U72 #U13 U12 #U12 U32 isNat U15 U61 #U11 U31 tt U13
#isNatKind(x1)	status: x1
   U41(x1,x2)	status: x1
 #U31(x1,x2,x3)	status: [x3,x1,x2]	precedence above:
 #U91(x1,x2)	status: []	precedence above:
 #U61(x1,x2)	status: []	precedence above:
    Usable rules: { 1..53 }
    Removed DPs: #17 #97
Number of SCCs: 0, DPs: 0, edges: 0
YES