Input TRS:
    1: a__U11(tt(),V1,V2) -> a__U12(a__isNatKind(V1),V1,V2)
    2: a__U12(tt(),V1,V2) -> a__U13(a__isNatKind(V2),V1,V2)
    3: a__U13(tt(),V1,V2) -> a__U14(a__isNatKind(V2),V1,V2)
    4: a__U14(tt(),V1,V2) -> a__U15(a__isNat(V1),V2)
    5: a__U15(tt(),V2) -> a__U16(a__isNat(V2))
    6: a__U16(tt()) -> tt()
    7: a__U21(tt(),V1) -> a__U22(a__isNatKind(V1),V1)
    8: a__U22(tt(),V1) -> a__U23(a__isNat(V1))
    9: a__U23(tt()) -> tt()
    10: a__U31(tt(),V2) -> a__U32(a__isNatKind(V2))
    11: a__U32(tt()) -> tt()
    12: a__U41(tt()) -> tt()
    13: a__U51(tt(),N) -> a__U52(a__isNatKind(N),N)
    14: a__U52(tt(),N) -> mark(N)
    15: a__U61(tt(),M,N) -> a__U62(a__isNatKind(M),M,N)
    16: a__U62(tt(),M,N) -> a__U63(a__isNat(N),M,N)
    17: a__U63(tt(),M,N) -> a__U64(a__isNatKind(N),M,N)
    18: a__U64(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
    19: a__isNat(0()) -> tt()
    20: a__isNat(plus(V1,V2)) -> a__U11(a__isNatKind(V1),V1,V2)
    21: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1)
    22: a__isNatKind(0()) -> tt()
    23: a__isNatKind(plus(V1,V2)) -> a__U31(a__isNatKind(V1),V2)
    24: a__isNatKind(s(V1)) -> a__U41(a__isNatKind(V1))
    25: a__plus(N,0()) -> a__U51(a__isNat(N),N)
    26: a__plus(N,s(M)) -> a__U61(a__isNat(M),M,N)
    27: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
    28: mark(U12(X1,X2,X3)) -> a__U12(mark(X1),X2,X3)
    29: mark(isNatKind(X)) -> a__isNatKind(X)
    30: mark(U13(X1,X2,X3)) -> a__U13(mark(X1),X2,X3)
    31: mark(U14(X1,X2,X3)) -> a__U14(mark(X1),X2,X3)
    32: mark(U15(X1,X2)) -> a__U15(mark(X1),X2)
    33: mark(isNat(X)) -> a__isNat(X)
    34: mark(U16(X)) -> a__U16(mark(X))
    35: mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
    36: mark(U22(X1,X2)) -> a__U22(mark(X1),X2)
    37: mark(U23(X)) -> a__U23(mark(X))
    38: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
    39: mark(U32(X)) -> a__U32(mark(X))
    40: mark(U41(X)) -> a__U41(mark(X))
    41: mark(U51(X1,X2)) -> a__U51(mark(X1),X2)
    42: mark(U52(X1,X2)) -> a__U52(mark(X1),X2)
    43: mark(U61(X1,X2,X3)) -> a__U61(mark(X1),X2,X3)
    44: mark(U62(X1,X2,X3)) -> a__U62(mark(X1),X2,X3)
    45: mark(U63(X1,X2,X3)) -> a__U63(mark(X1),X2,X3)
    46: mark(U64(X1,X2,X3)) -> a__U64(mark(X1),X2,X3)
    47: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
    48: mark(tt()) -> tt()
    49: mark(s(X)) -> s(mark(X))
    50: mark(0()) -> 0()
    51: a__U11(X1,X2,X3) -> U11(X1,X2,X3)
    52: a__U12(X1,X2,X3) -> U12(X1,X2,X3)
    53: a__isNatKind(X) -> isNatKind(X)
    54: a__U13(X1,X2,X3) -> U13(X1,X2,X3)
    55: a__U14(X1,X2,X3) -> U14(X1,X2,X3)
    56: a__U15(X1,X2) -> U15(X1,X2)
    57: a__isNat(X) -> isNat(X)
    58: a__U16(X) -> U16(X)
    59: a__U21(X1,X2) -> U21(X1,X2)
    60: a__U22(X1,X2) -> U22(X1,X2)
    61: a__U23(X) -> U23(X)
    62: a__U31(X1,X2) -> U31(X1,X2)
    63: a__U32(X) -> U32(X)
    64: a__U41(X) -> U41(X)
    65: a__U51(X1,X2) -> U51(X1,X2)
    66: a__U52(X1,X2) -> U52(X1,X2)
    67: a__U61(X1,X2,X3) -> U61(X1,X2,X3)
    68: a__U62(X1,X2,X3) -> U62(X1,X2,X3)
    69: a__U63(X1,X2,X3) -> U63(X1,X2,X3)
    70: a__U64(X1,X2,X3) -> U64(X1,X2,X3)
    71: a__plus(X1,X2) -> plus(X1,X2)
Number of strict rules: 71
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #a__U12(tt(),V1,V2) -> #a__U13(a__isNatKind(V2),V1,V2)
   #2: #a__U12(tt(),V1,V2) -> #a__isNatKind(V2)
   #3: #mark(U61(X1,X2,X3)) -> #a__U61(mark(X1),X2,X3)
   #4: #mark(U61(X1,X2,X3)) -> #mark(X1)
   #5: #mark(isNatKind(X)) -> #a__isNatKind(X)
   #6: #mark(U21(X1,X2)) -> #a__U21(mark(X1),X2)
   #7: #mark(U21(X1,X2)) -> #mark(X1)
   #8: #mark(U64(X1,X2,X3)) -> #a__U64(mark(X1),X2,X3)
   #9: #mark(U64(X1,X2,X3)) -> #mark(X1)
   #10: #mark(U52(X1,X2)) -> #a__U52(mark(X1),X2)
   #11: #mark(U52(X1,X2)) -> #mark(X1)
   #12: #mark(U51(X1,X2)) -> #a__U51(mark(X1),X2)
   #13: #mark(U51(X1,X2)) -> #mark(X1)
   #14: #mark(U23(X)) -> #a__U23(mark(X))
   #15: #mark(U23(X)) -> #mark(X)
   #16: #mark(plus(X1,X2)) -> #a__plus(mark(X1),mark(X2))
   #17: #mark(plus(X1,X2)) -> #mark(X1)
   #18: #mark(plus(X1,X2)) -> #mark(X2)
   #19: #mark(U31(X1,X2)) -> #a__U31(mark(X1),X2)
   #20: #mark(U31(X1,X2)) -> #mark(X1)
   #21: #mark(U41(X)) -> #a__U41(mark(X))
   #22: #mark(U41(X)) -> #mark(X)
   #23: #a__U51(tt(),N) -> #a__U52(a__isNatKind(N),N)
   #24: #a__U51(tt(),N) -> #a__isNatKind(N)
   #25: #a__isNatKind(s(V1)) -> #a__U41(a__isNatKind(V1))
   #26: #a__isNatKind(s(V1)) -> #a__isNatKind(V1)
   #27: #a__isNatKind(plus(V1,V2)) -> #a__U31(a__isNatKind(V1),V2)
   #28: #a__isNatKind(plus(V1,V2)) -> #a__isNatKind(V1)
   #29: #mark(U63(X1,X2,X3)) -> #a__U63(mark(X1),X2,X3)
   #30: #mark(U63(X1,X2,X3)) -> #mark(X1)
   #31: #mark(U14(X1,X2,X3)) -> #a__U14(mark(X1),X2,X3)
   #32: #mark(U14(X1,X2,X3)) -> #mark(X1)
   #33: #a__U52(tt(),N) -> #mark(N)
   #34: #mark(U13(X1,X2,X3)) -> #a__U13(mark(X1),X2,X3)
   #35: #mark(U13(X1,X2,X3)) -> #mark(X1)
   #36: #mark(s(X)) -> #mark(X)
   #37: #a__plus(N,0()) -> #a__U51(a__isNat(N),N)
   #38: #a__plus(N,0()) -> #a__isNat(N)
   #39: #a__isNat(plus(V1,V2)) -> #a__U11(a__isNatKind(V1),V1,V2)
   #40: #a__isNat(plus(V1,V2)) -> #a__isNatKind(V1)
   #41: #a__U21(tt(),V1) -> #a__U22(a__isNatKind(V1),V1)
   #42: #a__U21(tt(),V1) -> #a__isNatKind(V1)
   #43: #mark(U32(X)) -> #a__U32(mark(X))
   #44: #mark(U32(X)) -> #mark(X)
   #45: #a__U31(tt(),V2) -> #a__U32(a__isNatKind(V2))
   #46: #a__U31(tt(),V2) -> #a__isNatKind(V2)
   #47: #mark(isNat(X)) -> #a__isNat(X)
   #48: #a__U15(tt(),V2) -> #a__U16(a__isNat(V2))
   #49: #a__U15(tt(),V2) -> #a__isNat(V2)
   #50: #mark(U62(X1,X2,X3)) -> #a__U62(mark(X1),X2,X3)
   #51: #mark(U62(X1,X2,X3)) -> #mark(X1)
   #52: #mark(U12(X1,X2,X3)) -> #a__U12(mark(X1),X2,X3)
   #53: #mark(U12(X1,X2,X3)) -> #mark(X1)
   #54: #mark(U16(X)) -> #a__U16(mark(X))
   #55: #mark(U16(X)) -> #mark(X)
   #56: #mark(U11(X1,X2,X3)) -> #a__U11(mark(X1),X2,X3)
   #57: #mark(U11(X1,X2,X3)) -> #mark(X1)
   #58: #a__U63(tt(),M,N) -> #a__U64(a__isNatKind(N),M,N)
   #59: #a__U63(tt(),M,N) -> #a__isNatKind(N)
   #60: #mark(U15(X1,X2)) -> #a__U15(mark(X1),X2)
   #61: #mark(U15(X1,X2)) -> #mark(X1)
   #62: #a__plus(N,s(M)) -> #a__U61(a__isNat(M),M,N)
   #63: #a__plus(N,s(M)) -> #a__isNat(M)
   #64: #mark(U22(X1,X2)) -> #a__U22(mark(X1),X2)
   #65: #mark(U22(X1,X2)) -> #mark(X1)
   #66: #a__isNat(s(V1)) -> #a__U21(a__isNatKind(V1),V1)
   #67: #a__isNat(s(V1)) -> #a__isNatKind(V1)
   #68: #a__U62(tt(),M,N) -> #a__U63(a__isNat(N),M,N)
   #69: #a__U62(tt(),M,N) -> #a__isNat(N)
   #70: #a__U13(tt(),V1,V2) -> #a__U14(a__isNatKind(V2),V1,V2)
   #71: #a__U13(tt(),V1,V2) -> #a__isNatKind(V2)
   #72: #a__U11(tt(),V1,V2) -> #a__U12(a__isNatKind(V1),V1,V2)
   #73: #a__U11(tt(),V1,V2) -> #a__isNatKind(V1)
   #74: #a__U22(tt(),V1) -> #a__U23(a__isNat(V1))
   #75: #a__U22(tt(),V1) -> #a__isNat(V1)
   #76: #a__U61(tt(),M,N) -> #a__U62(a__isNatKind(M),M,N)
   #77: #a__U61(tt(),M,N) -> #a__isNatKind(M)
   #78: #a__U14(tt(),V1,V2) -> #a__U15(a__isNat(V1),V2)
   #79: #a__U14(tt(),V1,V2) -> #a__isNat(V1)
   #80: #a__U64(tt(),M,N) -> #a__plus(mark(N),mark(M))
   #81: #a__U64(tt(),M,N) -> #mark(N)
   #82: #a__U64(tt(),M,N) -> #mark(M)
Number of SCCs: 3, DPs: 52, edges: 716
	SCC { #26..28 #46 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#a__isNatKind(x1)	weight: x1
isNatKind(x1)	weight: (/ 1 4) + x1
a__U63(x1,x2,x3)	weight: 0
a__plus(x1,x2)	weight: 0
   U16(x1)	weight: 0
   U21(x1,x2)	weight: 0
#a__U15(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
   U64(x1,x2,x3)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
#a__U31(x1,x2)	weight: (/ 1 8) + x2
#a__U23(x1)	weight: 0
#a__isNat(x1)	weight: 0
#a__U14(x1,x2,x3)	weight: 0
a__U62(x1,x2,x3)	weight: 0
#a__U13(x1,x2,x3)	weight: 0
#a__U51(x1,x2)	weight: 0
   U23(x1)	weight: 0
   U63(x1,x2,x3)	weight: 0
a__U22(x1,x2)	weight: 0
a__U64(x1,x2,x3)	weight: 0
#a__U11(x1,x2,x3)	weight: 0
a__U31(x1,x2)	weight: (/ 1 4) + x2
a__U51(x1,x2)	weight: 0
   U12(x1,x2,x3)	weight: 0
#a__U62(x1,x2,x3)	weight: 0
a__U16(x1)	weight: 0
a__U41(x1)	weight: (/ 1 4)
#a__U64(x1,x2,x3)	weight: 0
#a__U12(x1,x2,x3)	weight: 0
a__U14(x1,x2,x3)	weight: 0
#a__U21(x1,x2)	weight: 0
#a__U61(x1,x2,x3)	weight: 0
#a__plus(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
a__U21(x1,x2)	weight: 0
a__U32(x1)	weight: (/ 3 8)
   U62(x1,x2,x3)	weight: 0
#a__U52(x1,x2)	weight: 0
  mark(x1)	weight: 0
a__U11(x1,x2,x3)	weight: 0
   U32(x1)	weight: (/ 1 2) + x1
a__U52(x1,x2)	weight: 0
   U14(x1,x2,x3)	weight: 0
a__U12(x1,x2,x3)	weight: 0
#a__U63(x1,x2,x3)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2)	weight: 0
  plus(x1,x2)	weight: (/ 1 4) + x1 + x2
   U15(x1,x2)	weight: 0
   U61(x1,x2,x3)	weight: 0
#a__U22(x1,x2)	weight: 0
a__U13(x1,x2,x3)	weight: 0
   U31(x1,x2)	weight: (/ 3 8) + x1
a__U61(x1,x2,x3)	weight: 0
#a__U41(x1)	weight: 0
a__U15(x1,x2)	weight: 0
#a__U16(x1)	weight: 0
    tt()	weight: 0
a__isNat(x1)	weight: 0
   U13(x1,x2,x3)	weight: 0
a__U23(x1)	weight: 0
a__isNatKind(x1)	weight: (/ 1 8)
   U22(x1,x2)	weight: 0
   U51(x1,x2)	weight: 0
   U41(x1)	weight: (/ 3 8) + x1
#a__U32(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #26..28 #46
Number of SCCs: 2, DPs: 48, edges: 706
	SCC { #1 #39 #41 #49 #66 #70 #72 #75 #78 #79 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#a__isNatKind(x1)	weight: 0
isNatKind(x1)	weight: (/ 1 4) + x1
a__U63(x1,x2,x3)	weight: 0
a__plus(x1,x2)	weight: 0
   U16(x1)	weight: (/ 7 8) + x1
   U21(x1,x2)	weight: (/ 3 8) + x1 + x2
#a__U15(x1,x2)	weight: (/ 1 8) + x2
   U11(x1,x2,x3)	weight: (/ 3 8) + x2 + x3
   U64(x1,x2,x3)	weight: 0
     s(x1)	weight: (/ 3 8) + x1
#a__U31(x1,x2)	weight: (/ 1 8)
#a__U23(x1)	weight: 0
#a__isNat(x1)	weight: x1
#a__U14(x1,x2,x3)	weight: (/ 1 4) + x2 + x3
a__U62(x1,x2,x3)	weight: 0
#a__U13(x1,x2,x3)	weight: (/ 3 8) + x2 + x3
#a__U51(x1,x2)	weight: 0
   U23(x1)	weight: (/ 1 2)
   U63(x1,x2,x3)	weight: 0
a__U22(x1,x2)	weight: (/ 1 4) + x1 + x2
a__U64(x1,x2,x3)	weight: 0
#a__U11(x1,x2,x3)	weight: (/ 5 8) + x2 + x3
a__U31(x1,x2)	weight: (/ 1 4) + x2
a__U51(x1,x2)	weight: 0
   U12(x1,x2,x3)	weight: (/ 3 8) + x2 + x3
#a__U62(x1,x2,x3)	weight: 0
a__U16(x1)	weight: (/ 3 4)
a__U41(x1)	weight: (/ 1 4)
#a__U64(x1,x2,x3)	weight: 0
#a__U12(x1,x2,x3)	weight: (/ 1 2) + x2 + x3
a__U14(x1,x2,x3)	weight: (/ 1 2)
#a__U21(x1,x2)	weight: (/ 1 4) + x2
#a__U61(x1,x2,x3)	weight: 0
#a__plus(x1,x2)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
a__U21(x1,x2)	weight: (/ 1 4)
a__U32(x1)	weight: (/ 3 8)
   U62(x1,x2,x3)	weight: 0
#a__U52(x1,x2)	weight: 0
  mark(x1)	weight: 0
a__U11(x1,x2,x3)	weight: (/ 1 4)
   U32(x1)	weight: (/ 1 2)
a__U52(x1,x2)	weight: 0
   U14(x1,x2,x3)	weight: (/ 5 8) + x1 + x2
a__U12(x1,x2,x3)	weight: (/ 1 4) + x1
#a__U63(x1,x2,x3)	weight: 0
 isNat(x1)	weight: (/ 1 4) + x1
   U52(x1,x2)	weight: 0
  plus(x1,x2)	weight: (/ 3 4) + x1 + x2
   U15(x1,x2)	weight: (/ 3 4) + x1
   U61(x1,x2,x3)	weight: 0
#a__U22(x1,x2)	weight: (/ 1 8) + x2
a__U13(x1,x2,x3)	weight: (/ 3 8) + x2 + x3
   U31(x1,x2)	weight: (/ 3 8)
a__U61(x1,x2,x3)	weight: 0
#a__U41(x1)	weight: 0
a__U15(x1,x2)	weight: (/ 5 8) + x2
#a__U16(x1)	weight: 0
    tt()	weight: 0
a__isNat(x1)	weight: (/ 1 8)
   U13(x1,x2,x3)	weight: (/ 1 2) + x1
a__U23(x1)	weight: (/ 3 8)
a__isNatKind(x1)	weight: (/ 1 8)
   U22(x1,x2)	weight: (/ 3 8)
   U51(x1,x2)	weight: 0
   U41(x1)	weight: (/ 3 8) + x1
#a__U32(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #1 #39 #41 #49 #66 #70 #72 #75 #78 #79
Number of SCCs: 1, DPs: 38, edges: 692
	SCC { #3 #4 #7..13 #15..18 #20 #22 #23 #29 #30 #32 #33 #35..37 #44 #50 #51 #53 #55 #57 #58 #61 #62 #65 #68 #76 #80..82 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#a__isNatKind(x1)	weight: 0
isNatKind(x1)	weight: 0
a__U63(x1,x2,x3)	weight: (/ 9 8) + x1 + x2 + x3
a__plus(x1,x2)	weight: (/ 1 2) + x1 + x2
   U16(x1)	weight: x1
   U21(x1,x2)	weight: x1
#a__U15(x1,x2)	weight: (/ 1 8)
   U11(x1,x2,x3)	weight: x1
   U64(x1,x2,x3)	weight: (/ 9 8) + x1 + x2 + x3
     s(x1)	weight: (/ 5 8) + x1
#a__U31(x1,x2)	weight: (/ 1 8)
#a__U23(x1)	weight: 0
#a__isNat(x1)	weight: 0
#a__U14(x1,x2,x3)	weight: (/ 1 4)
a__U62(x1,x2,x3)	weight: (/ 9 8) + x1 + x2 + x3
#a__U13(x1,x2,x3)	weight: (/ 3 8)
#a__U51(x1,x2)	weight: (/ 1 4) + x2
   U23(x1)	weight: x1
   U63(x1,x2,x3)	weight: (/ 9 8) + x1 + x2 + x3
a__U22(x1,x2)	weight: x1
a__U64(x1,x2,x3)	weight: (/ 9 8) + x1 + x2 + x3
#a__U11(x1,x2,x3)	weight: (/ 5 8)
a__U31(x1,x2)	weight: x1
a__U51(x1,x2)	weight: (/ 3 8) + x1 + x2
   U12(x1,x2,x3)	weight: x1
#a__U62(x1,x2,x3)	weight: (/ 3 4) + x2 + x3
a__U16(x1)	weight: x1
a__U41(x1)	weight: x1
#a__U64(x1,x2,x3)	weight: (/ 1 2) + x2 + x3
#a__U12(x1,x2,x3)	weight: (/ 1 2)
a__U14(x1,x2,x3)	weight: x1
#a__U21(x1,x2)	weight: (/ 1 4)
#a__U61(x1,x2,x3)	weight: (/ 7 8) + x2 + x3
#a__plus(x1,x2)	weight: (/ 3 8) + x1 + x2
#mark(x1)	weight: x1
     0()	weight: 0
a__U21(x1,x2)	weight: x1
a__U32(x1)	weight: x1
   U62(x1,x2,x3)	weight: (/ 9 8) + x1 + x2 + x3
#a__U52(x1,x2)	weight: (/ 1 8) + x2
  mark(x1)	weight: x1
a__U11(x1,x2,x3)	weight: x1
   U32(x1)	weight: x1
a__U52(x1,x2)	weight: (/ 1 4) + x1 + x2
   U14(x1,x2,x3)	weight: x1
a__U12(x1,x2,x3)	weight: x1
#a__U63(x1,x2,x3)	weight: (/ 5 8) + x2 + x3
 isNat(x1)	weight: 0
   U52(x1,x2)	weight: (/ 1 4) + x1 + x2
  plus(x1,x2)	weight: (/ 1 2) + x1 + x2
   U15(x1,x2)	weight: x1
   U61(x1,x2,x3)	weight: (/ 9 8) + x1 + x2 + x3
#a__U22(x1,x2)	weight: (/ 1 8)
a__U13(x1,x2,x3)	weight: x1
   U31(x1,x2)	weight: x1
a__U61(x1,x2,x3)	weight: (/ 9 8) + x1 + x2 + x3
#a__U41(x1)	weight: 0
a__U15(x1,x2)	weight: x1
#a__U16(x1)	weight: 0
    tt()	weight: 0
a__isNat(x1)	weight: 0
   U13(x1,x2,x3)	weight: x1
a__U23(x1)	weight: x1
a__isNatKind(x1)	weight: 0
   U22(x1,x2)	weight: x1
   U51(x1,x2)	weight: (/ 3 8) + x1 + x2
   U41(x1)	weight: x1
#a__U32(x1)	weight: 0
    Usable rules: { 1..71 }
    Removed DPs: #3 #4 #8..13 #16..18 #23 #29 #30 #33 #36 #37 #50 #51 #58 #62 #68 #76 #80..82
Number of SCCs: 1, DPs: 12, edges: 144
	SCC { #7 #15 #20 #22 #32 #35 #44 #53 #55 #57 #61 #65 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#a__isNatKind(x1)	weight: 0
isNatKind(x1)	weight: 0
a__U63(x1,x2,x3)	weight: (/ 11 16) + x1 + x2 + x3
a__plus(x1,x2)	weight: (/ 1 4) + x1 + x2
   U16(x1)	weight: (/ 1 16) + x1
   U21(x1,x2)	weight: (/ 1 16) + x1
#a__U15(x1,x2)	weight: (/ 1 16)
   U11(x1,x2,x3)	weight: (/ 1 16) + x1
   U64(x1,x2,x3)	weight: x1 + x2 + x3
     s(x1)	weight: (/ 5 16) + x1
#a__U31(x1,x2)	weight: (/ 1 16)
#a__U23(x1)	weight: 0
#a__isNat(x1)	weight: 0
#a__U14(x1,x2,x3)	weight: (/ 1 8)
a__U62(x1,x2,x3)	weight: (/ 3 4) + x1 + x2 + x3
#a__U13(x1,x2,x3)	weight: (/ 3 16)
#a__U51(x1,x2)	weight: (/ 1 8)
   U23(x1)	weight: (/ 1 16) + x1
   U63(x1,x2,x3)	weight: x1 + x2 + x3
a__U22(x1,x2)	weight: (/ 1 16)
a__U64(x1,x2,x3)	weight: (/ 11 16) + x1 + x2 + x3
#a__U11(x1,x2,x3)	weight: (/ 5 16)
a__U31(x1,x2)	weight: x1
a__U51(x1,x2)	weight: (/ 1 16) + x2
   U12(x1,x2,x3)	weight: (/ 1 16) + x1
#a__U62(x1,x2,x3)	weight: (/ 3 8)
a__U16(x1)	weight: (/ 1 16) + x1
a__U41(x1)	weight: (/ 1 16)
#a__U64(x1,x2,x3)	weight: (/ 1 4)
#a__U12(x1,x2,x3)	weight: (/ 1 4)
a__U14(x1,x2,x3)	weight: (/ 1 16) + x1
#a__U21(x1,x2)	weight: (/ 1 8)
#a__U61(x1,x2,x3)	weight: (/ 7 16)
#a__plus(x1,x2)	weight: (/ 3 16)
#mark(x1)	weight: x1
     0()	weight: 0
a__U21(x1,x2)	weight: (/ 1 16)
a__U32(x1)	weight: (/ 1 16) + x1
   U62(x1,x2,x3)	weight: x1 + x2 + x3
#a__U52(x1,x2)	weight: (/ 1 16)
  mark(x1)	weight: (/ 1 16)
a__U11(x1,x2,x3)	weight: (/ 1 16) + x1
   U32(x1)	weight: (/ 1 16) + x1
a__U52(x1,x2)	weight: (/ 1 16) + x2
   U14(x1,x2,x3)	weight: (/ 1 16) + x1
a__U12(x1,x2,x3)	weight: (/ 1 16) + x1
#a__U63(x1,x2,x3)	weight: (/ 5 16)
 isNat(x1)	weight: 0
   U52(x1,x2)	weight: x2
  plus(x1,x2)	weight: (/ 1 16) + x1 + x2
   U15(x1,x2)	weight: (/ 1 16) + x1
   U61(x1,x2,x3)	weight: x1 + x2 + x3
#a__U22(x1,x2)	weight: (/ 1 16)
a__U13(x1,x2,x3)	weight: (/ 1 16) + x1
   U31(x1,x2)	weight: (/ 1 16) + x1
a__U61(x1,x2,x3)	weight: x1 + x2
#a__U41(x1)	weight: 0
a__U15(x1,x2)	weight: x1
#a__U16(x1)	weight: 0
    tt()	weight: 0
a__isNat(x1)	weight: (/ 1 16)
   U13(x1,x2,x3)	weight: (/ 1 16) + x1
a__U23(x1)	weight: (/ 1 16)
a__isNatKind(x1)	weight: 0
   U22(x1,x2)	weight: (/ 1 16) + x1
   U51(x1,x2)	weight: x2
   U41(x1)	weight: (/ 1 16) + x1
#a__U32(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #7 #15 #20 #22 #32 #35 #44 #53 #55 #57 #61 #65
Number of SCCs: 0, DPs: 0, edges: 0
YES