Input TRS:
    1: a__U11(tt(),V1,V2) -> a__U12(a__isNat(V1),V2)
    2: a__U12(tt(),V2) -> a__U13(a__isNat(V2))
    3: a__U13(tt()) -> tt()
    4: a__U21(tt(),V1) -> a__U22(a__isNat(V1))
    5: a__U22(tt()) -> tt()
    6: a__U31(tt(),V1,V2) -> a__U32(a__isNat(V1),V2)
    7: a__U32(tt(),V2) -> a__U33(a__isNat(V2))
    8: a__U33(tt()) -> tt()
    9: a__U41(tt(),N) -> mark(N)
    10: a__U51(tt(),M,N) -> s(a__plus(mark(N),mark(M)))
    11: a__U61(tt()) -> |0|()
    12: a__U71(tt(),M,N) -> a__plus(a__x(mark(N),mark(M)),mark(N))
    13: a__and(tt(),X) -> mark(X)
    14: a__isNat(|0|()) -> tt()
    15: a__isNat(plus(V1,V2)) -> a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)
    16: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1)
    17: a__isNat(x(V1,V2)) -> a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)
    18: a__isNatKind(|0|()) -> tt()
    19: a__isNatKind(plus(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2))
    20: a__isNatKind(s(V1)) -> a__isNatKind(V1)
    21: a__isNatKind(x(V1,V2)) -> a__and(a__isNatKind(V1),isNatKind(V2))
    22: a__plus(N,|0|()) -> a__U41(a__and(a__isNat(N),isNatKind(N)),N)
    23: a__plus(N,s(M)) -> a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)
    24: a__x(N,|0|()) -> a__U61(a__and(a__isNat(N),isNatKind(N)))
    25: a__x(N,s(M)) -> a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)
    26: mark(U11(X1,X2,X3)) -> a__U11(mark(X1),X2,X3)
    27: mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
    28: mark(isNat(X)) -> a__isNat(X)
    29: mark(U13(X)) -> a__U13(mark(X))
    30: mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
    31: mark(U22(X)) -> a__U22(mark(X))
    32: mark(U31(X1,X2,X3)) -> a__U31(mark(X1),X2,X3)
    33: mark(U32(X1,X2)) -> a__U32(mark(X1),X2)
    34: mark(U33(X)) -> a__U33(mark(X))
    35: mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
    36: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
    37: mark(plus(X1,X2)) -> a__plus(mark(X1),mark(X2))
    38: mark(U61(X)) -> a__U61(mark(X))
    39: mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
    40: mark(x(X1,X2)) -> a__x(mark(X1),mark(X2))
    41: mark(and(X1,X2)) -> a__and(mark(X1),X2)
    42: mark(isNatKind(X)) -> a__isNatKind(X)
    43: mark(tt()) -> tt()
    44: mark(s(X)) -> s(mark(X))
    45: mark(|0|()) -> |0|()
    46: a__U11(X1,X2,X3) -> U11(X1,X2,X3)
    47: a__U12(X1,X2) -> U12(X1,X2)
    48: a__isNat(X) -> isNat(X)
    49: a__U13(X) -> U13(X)
    50: a__U21(X1,X2) -> U21(X1,X2)
    51: a__U22(X) -> U22(X)
    52: a__U31(X1,X2,X3) -> U31(X1,X2,X3)
    53: a__U32(X1,X2) -> U32(X1,X2)
    54: a__U33(X) -> U33(X)
    55: a__U41(X1,X2) -> U41(X1,X2)
    56: a__U51(X1,X2,X3) -> U51(X1,X2,X3)
    57: a__plus(X1,X2) -> plus(X1,X2)
    58: a__U61(X) -> U61(X)
    59: a__U71(X1,X2,X3) -> U71(X1,X2,X3)
    60: a__x(X1,X2) -> x(X1,X2)
    61: a__and(X1,X2) -> and(X1,X2)
    62: a__isNatKind(X) -> isNatKind(X)
Number of strict rules: 62
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #a__U12(tt(),V2) -> #a__U13(a__isNat(V2))
   #2: #a__U12(tt(),V2) -> #a__isNat(V2)
   #3: #mark(U13(X)) -> #a__U13(mark(X))
   #4: #mark(U13(X)) -> #mark(X)
   #5: #mark(U41(X1,X2)) -> #a__U41(mark(X1),X2)
   #6: #mark(U41(X1,X2)) -> #mark(X1)
   #7: #mark(isNatKind(X)) -> #a__isNatKind(X)
   #8: #mark(and(X1,X2)) -> #a__and(mark(X1),X2)
   #9: #mark(and(X1,X2)) -> #mark(X1)
   #10: #mark(plus(X1,X2)) -> #a__plus(mark(X1),mark(X2))
   #11: #mark(plus(X1,X2)) -> #mark(X1)
   #12: #mark(plus(X1,X2)) -> #mark(X2)
   #13: #mark(U61(X)) -> #a__U61(mark(X))
   #14: #mark(U61(X)) -> #mark(X)
   #15: #a__U31(tt(),V1,V2) -> #a__U32(a__isNat(V1),V2)
   #16: #a__U31(tt(),V1,V2) -> #a__isNat(V1)
   #17: #mark(x(X1,X2)) -> #a__x(mark(X1),mark(X2))
   #18: #mark(x(X1,X2)) -> #mark(X1)
   #19: #mark(x(X1,X2)) -> #mark(X2)
   #20: #a__and(tt(),X) -> #mark(X)
   #21: #a__U41(tt(),N) -> #mark(N)
   #22: #a__x(N,|0|()) -> #a__U61(a__and(a__isNat(N),isNatKind(N)))
   #23: #a__x(N,|0|()) -> #a__and(a__isNat(N),isNatKind(N))
   #24: #a__x(N,|0|()) -> #a__isNat(N)
   #25: #a__plus(N,s(M)) -> #a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)
   #26: #a__plus(N,s(M)) -> #a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))
   #27: #a__plus(N,s(M)) -> #a__and(a__isNat(M),isNatKind(M))
   #28: #a__plus(N,s(M)) -> #a__isNat(M)
   #29: #a__U71(tt(),M,N) -> #a__plus(a__x(mark(N),mark(M)),mark(N))
   #30: #a__U71(tt(),M,N) -> #a__x(mark(N),mark(M))
   #31: #a__U71(tt(),M,N) -> #mark(N)
   #32: #a__U71(tt(),M,N) -> #mark(M)
   #33: #a__U71(tt(),M,N) -> #mark(N)
   #34: #mark(U22(X)) -> #a__U22(mark(X))
   #35: #mark(U22(X)) -> #mark(X)
   #36: #mark(U21(X1,X2)) -> #a__U21(mark(X1),X2)
   #37: #mark(U21(X1,X2)) -> #mark(X1)
   #38: #a__x(N,s(M)) -> #a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)
   #39: #a__x(N,s(M)) -> #a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))
   #40: #a__x(N,s(M)) -> #a__and(a__isNat(M),isNatKind(M))
   #41: #a__x(N,s(M)) -> #a__isNat(M)
   #42: #a__isNatKind(s(V1)) -> #a__isNatKind(V1)
   #43: #a__U32(tt(),V2) -> #a__U33(a__isNat(V2))
   #44: #a__U32(tt(),V2) -> #a__isNat(V2)
   #45: #mark(U71(X1,X2,X3)) -> #a__U71(mark(X1),X2,X3)
   #46: #mark(U71(X1,X2,X3)) -> #mark(X1)
   #47: #a__U51(tt(),M,N) -> #a__plus(mark(N),mark(M))
   #48: #a__U51(tt(),M,N) -> #mark(N)
   #49: #a__U51(tt(),M,N) -> #mark(M)
   #50: #mark(U32(X1,X2)) -> #a__U32(mark(X1),X2)
   #51: #mark(U32(X1,X2)) -> #mark(X1)
   #52: #mark(s(X)) -> #mark(X)
   #53: #mark(isNat(X)) -> #a__isNat(X)
   #54: #a__plus(N,|0|()) -> #a__U41(a__and(a__isNat(N),isNatKind(N)),N)
   #55: #a__plus(N,|0|()) -> #a__and(a__isNat(N),isNatKind(N))
   #56: #a__plus(N,|0|()) -> #a__isNat(N)
   #57: #mark(U33(X)) -> #a__U33(mark(X))
   #58: #mark(U33(X)) -> #mark(X)
   #59: #mark(U12(X1,X2)) -> #a__U12(mark(X1),X2)
   #60: #mark(U12(X1,X2)) -> #mark(X1)
   #61: #a__isNat(x(V1,V2)) -> #a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)
   #62: #a__isNat(x(V1,V2)) -> #a__and(a__isNatKind(V1),isNatKind(V2))
   #63: #a__isNat(x(V1,V2)) -> #a__isNatKind(V1)
   #64: #mark(U31(X1,X2,X3)) -> #a__U31(mark(X1),X2,X3)
   #65: #mark(U31(X1,X2,X3)) -> #mark(X1)
   #66: #a__isNatKind(plus(V1,V2)) -> #a__and(a__isNatKind(V1),isNatKind(V2))
   #67: #a__isNatKind(plus(V1,V2)) -> #a__isNatKind(V1)
   #68: #mark(U11(X1,X2,X3)) -> #a__U11(mark(X1),X2,X3)
   #69: #mark(U11(X1,X2,X3)) -> #mark(X1)
   #70: #mark(U51(X1,X2,X3)) -> #a__U51(mark(X1),X2,X3)
   #71: #mark(U51(X1,X2,X3)) -> #mark(X1)
   #72: #a__isNatKind(x(V1,V2)) -> #a__and(a__isNatKind(V1),isNatKind(V2))
   #73: #a__isNatKind(x(V1,V2)) -> #a__isNatKind(V1)
   #74: #a__isNat(s(V1)) -> #a__U21(a__isNatKind(V1),V1)
   #75: #a__isNat(s(V1)) -> #a__isNatKind(V1)
   #76: #a__U11(tt(),V1,V2) -> #a__U12(a__isNat(V1),V2)
   #77: #a__U11(tt(),V1,V2) -> #a__isNat(V1)
   #78: #a__isNat(plus(V1,V2)) -> #a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)
   #79: #a__isNat(plus(V1,V2)) -> #a__and(a__isNatKind(V1),isNatKind(V2))
   #80: #a__isNat(plus(V1,V2)) -> #a__isNatKind(V1)
   #81: #a__U21(tt(),V1) -> #a__U22(a__isNat(V1))
   #82: #a__U21(tt(),V1) -> #a__isNat(V1)
Number of SCCs: 1, DPs: 74, edges: 966
	SCC { #2 #4..12 #14..21 #23..33 #35..42 #44..56 #58..80 #82 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: (/ 1 8)
#a__isNatKind(x1)	weight: (/ 1 8)
isNatKind(x1)	weight: 0
a__plus(x1,x2)	weight: max{(/ 5 8) + x2, x1}
   U21(x1,x2)	weight: max{x2, x1}
#a__U71(x1,x2,x3)	weight: max{0, (/ 3 4) + x3, (/ 1 2) + x2}
   U11(x1,x2,x3)	weight: max{(/ 5 8) + x3, x2, (/ 1 2) + x1}
     s(x1)	weight: x1
#a__U31(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 3 8) + x2}
#a__U33(x1)	weight: 0
a__U33(x1)	weight: (/ 3 8) + x1
#a__isNat(x1)	weight: (/ 1 8) + x1
   U71(x1,x2,x3)	weight: max{(/ 5 8) + x3, (/ 3 8) + x2, (/ 1 4) + x1}
   and(x1,x2)	weight: max{x2, x1}
#a__U13(x1)	weight: 0
#a__U51(x1,x2,x3)	weight: max{0, (/ 1 8) + x3, (/ 3 4) + x2}
#a__x(x1,x2)	weight: max{(/ 1 2) + x2, (/ 3 4) + x1}
a__U22(x1)	weight: x1
#a__U11(x1,x2,x3)	weight: max{0, (/ 3 4) + x3, (/ 1 8) + x2}
a__U31(x1,x2,x3)	weight: max{(/ 3 8) + x3, (/ 1 2) + x2, (/ 5 8) + x1}
a__U51(x1,x2,x3)	weight: max{x3, (/ 5 8) + x2, x1}
  a__x(x1,x2)	weight: max{(/ 3 8) + x2, (/ 5 8) + x1}
   U12(x1,x2)	weight: max{(/ 5 8) + x2, x1}
a__U41(x1,x2)	weight: max{x2, x1}
     x(x1,x2)	weight: max{(/ 3 8) + x2, (/ 5 8) + x1}
#a__U12(x1,x2)	weight: max{0, (/ 1 4) + x2}
#a__U21(x1,x2)	weight: max{0, (/ 1 8) + x2}
#a__U61(x1)	weight: 0
#a__plus(x1,x2)	weight: max{(/ 3 4) + x2, (/ 1 8) + x1}
#mark(x1)	weight: (/ 1 8) + x1
#a__and(x1,x2)	weight: max{0, (/ 1 8) + x2}
a__U21(x1,x2)	weight: max{x2, x1}
a__U32(x1,x2)	weight: max{(/ 3 8) + x2, (/ 1 2) + x1}
  mark(x1)	weight: x1
a__U11(x1,x2,x3)	weight: max{(/ 5 8) + x3, x2, (/ 1 2) + x1}
   U32(x1,x2)	weight: max{(/ 3 8) + x2, (/ 1 2) + x1}
   U33(x1)	weight: (/ 3 8) + x1
a__U12(x1,x2)	weight: max{(/ 5 8) + x2, x1}
 isNat(x1)	weight: x1
  plus(x1,x2)	weight: max{(/ 5 8) + x2, x1}
   U61(x1)	weight: (/ 5 8) + x1
#a__U22(x1)	weight: 0
a__U13(x1)	weight: (/ 1 8) + x1
   U31(x1,x2,x3)	weight: max{(/ 3 8) + x3, (/ 1 2) + x2, (/ 5 8) + x1}
a__U71(x1,x2,x3)	weight: max{(/ 5 8) + x3, (/ 3 8) + x2, (/ 1 4) + x1}
a__U61(x1)	weight: (/ 5 8) + x1
#a__U41(x1,x2)	weight: max{0, (/ 1 8) + x2}
    tt()	weight: 0
a__isNat(x1)	weight: x1
   U13(x1)	weight: (/ 1 8) + x1
a__isNatKind(x1)	weight: 0
   U22(x1)	weight: x1
   U51(x1,x2,x3)	weight: max{x3, (/ 5 8) + x2, x1}
a__and(x1,x2)	weight: max{x2, x1}
   U41(x1,x2)	weight: max{x2, x1}
#a__U32(x1,x2)	weight: max{0, (/ 1 4) + x2}
    Usable rules: { 1..62 }
    Removed DPs: #2 #4 #12 #14..16 #18 #19 #23 #24 #27 #28 #31..33 #39..41 #44 #46 #49..51 #55 #58 #59 #61..65 #69 #76 #79 #80
Number of SCCs: 1, DPs: 39, edges: 267
	SCC { #5..11 #17 #20 #21 #25 #26 #29 #30 #35..38 #42 #45 #47 #48 #52..54 #56 #60 #66..68 #70..75 #77 #78 #82 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: (/ 1 8)
#a__isNatKind(x1)	weight: (/ 1 8)
isNatKind(x1)	weight: 0
a__plus(x1,x2)	weight: max{(/ 3 8) + x2, x1}
   U21(x1,x2)	weight: max{x2, x1}
#a__U71(x1,x2,x3)	weight: max{0, (/ 1 2) + x3, (/ 1 4) + x2}
   U11(x1,x2,x3)	weight: max{(/ 1 4) + x3, x2, (/ 1 8) + x1}
     s(x1)	weight: x1
#a__U31(x1,x2,x3)	weight: 0
#a__U33(x1)	weight: 0
a__U33(x1)	weight: (/ 1 8) + x1
#a__isNat(x1)	weight: (/ 1 8)
   U71(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 1 8) + x2}
   and(x1,x2)	weight: max{x2, x1}
#a__U13(x1)	weight: 0
#a__U51(x1,x2,x3)	weight: max{0, (/ 1 8) + x3, (/ 1 2) + x2}
#a__x(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 2) + x1}
a__U22(x1)	weight: x1
#a__U11(x1,x2,x3)	weight: max{0, (/ 1 8) + x1}
a__U31(x1,x2,x3)	weight: max{(/ 1 8) + x3, (/ 1 4) + x2, (/ 3 8) + x1}
a__U51(x1,x2,x3)	weight: max{x3, (/ 3 8) + x2, x1}
  a__x(x1,x2)	weight: max{(/ 1 8) + x2, (/ 3 8) + x1}
   U12(x1,x2)	weight: max{(/ 1 4) + x2, x1}
a__U41(x1,x2)	weight: max{x2, x1}
     x(x1,x2)	weight: max{(/ 1 8) + x2, (/ 3 8) + x1}
#a__U12(x1,x2)	weight: 0
#a__U21(x1,x2)	weight: max{0, (/ 1 8) + x1}
#a__U61(x1)	weight: 0
#a__plus(x1,x2)	weight: max{(/ 1 2) + x2, (/ 1 8) + x1}
#mark(x1)	weight: (/ 1 8) + x1
#a__and(x1,x2)	weight: max{0, (/ 1 8) + x2}
a__U21(x1,x2)	weight: max{x2, x1}
a__U32(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 4) + x1}
  mark(x1)	weight: x1
a__U11(x1,x2,x3)	weight: max{(/ 1 4) + x3, x2, (/ 1 8) + x1}
   U32(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 4) + x1}
   U33(x1)	weight: (/ 1 8) + x1
a__U12(x1,x2)	weight: max{(/ 1 4) + x2, x1}
 isNat(x1)	weight: x1
  plus(x1,x2)	weight: max{(/ 3 8) + x2, x1}
   U61(x1)	weight: (/ 3 8) + x1
#a__U22(x1)	weight: 0
a__U13(x1)	weight: (/ 1 8) + x1
   U31(x1,x2,x3)	weight: max{(/ 1 8) + x3, (/ 1 4) + x2, (/ 3 8) + x1}
a__U71(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 1 8) + x2}
a__U61(x1)	weight: (/ 3 8) + x1
#a__U41(x1,x2)	weight: max{0, (/ 1 8) + x2}
    tt()	weight: 0
a__isNat(x1)	weight: x1
   U13(x1)	weight: (/ 1 8) + x1
a__isNatKind(x1)	weight: 0
   U22(x1)	weight: x1
   U51(x1,x2,x3)	weight: max{x3, (/ 3 8) + x2, x1}
a__and(x1,x2)	weight: max{x2, x1}
   U41(x1,x2)	weight: max{x2, x1}
#a__U32(x1,x2)	weight: 0
    Usable rules: { 1..62 }
    Removed DPs: #56 #68
Number of SCCs: 1, DPs: 37, edges: 249
	SCC { #5..11 #17 #20 #21 #25 #26 #29 #30 #35..38 #42 #45 #47 #48 #52..54 #60 #66 #67 #70..75 #77 #78 #82 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: (/ 1 4)
#a__isNatKind(x1)	weight: (/ 1 2) + x1
isNatKind(x1)	weight: x1
a__plus(x1,x2)	weight: max{x2, x1}
   U21(x1,x2)	weight: max{x2, x1}
#a__U71(x1,x2,x3)	weight: max{0, (/ 3 4) + x3, (/ 7 8) + x2}
   U11(x1,x2,x3)	weight: max{0, x2}
     s(x1)	weight: x1
#a__U31(x1,x2,x3)	weight: 0
#a__U33(x1)	weight: 0
a__U33(x1)	weight: (/ 1 4)
#a__isNat(x1)	weight: (/ 1 2) + x1
   U71(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, (/ 3 8) + x2}
   and(x1,x2)	weight: max{x2, x1}
#a__U13(x1)	weight: 0
#a__U51(x1,x2,x3)	weight: max{0, (/ 1 2) + x3, (/ 1 8) + x2}
#a__x(x1,x2)	weight: max{(/ 7 8) + x2, (/ 3 4) + x1}
a__U22(x1)	weight: x1
#a__U11(x1,x2,x3)	weight: max{0, (/ 1 2) + x2}
a__U31(x1,x2,x3)	weight: max{0, (/ 1 4) + x2}
a__U51(x1,x2,x3)	weight: max{x3, x2, x1}
  a__x(x1,x2)	weight: max{(/ 3 8) + x2, (/ 1 4) + x1}
   U12(x1,x2)	weight: max{0, x1}
a__U41(x1,x2)	weight: max{x2, x1}
     x(x1,x2)	weight: max{(/ 3 8) + x2, (/ 1 4) + x1}
#a__U12(x1,x2)	weight: 0
#a__U21(x1,x2)	weight: max{(/ 1 2) + x2, (/ 3 8) + x1}
#a__U61(x1)	weight: 0
#a__plus(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 2) + x1}
#mark(x1)	weight: (/ 1 2) + x1
#a__and(x1,x2)	weight: max{0, (/ 1 2) + x2}
a__U21(x1,x2)	weight: max{x2, x1}
a__U32(x1,x2)	weight: max{0, (/ 1 8) + x1}
  mark(x1)	weight: x1
a__U11(x1,x2,x3)	weight: max{0, x2}
   U32(x1,x2)	weight: max{0, (/ 1 8) + x1}
   U33(x1)	weight: (/ 1 4)
a__U12(x1,x2)	weight: max{0, x1}
 isNat(x1)	weight: x1
  plus(x1,x2)	weight: max{x2, x1}
   U61(x1)	weight: (/ 1 4)
#a__U22(x1)	weight: 0
a__U13(x1)	weight: (/ 1 4)
   U31(x1,x2,x3)	weight: max{0, (/ 1 4) + x2}
a__U71(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, (/ 3 8) + x2}
a__U61(x1)	weight: (/ 1 4)
#a__U41(x1,x2)	weight: max{0, (/ 1 2) + x2}
    tt()	weight: (/ 1 4)
a__isNat(x1)	weight: x1
   U13(x1)	weight: (/ 1 4)
a__isNatKind(x1)	weight: x1
   U22(x1)	weight: x1
   U51(x1,x2,x3)	weight: max{x3, x2, x1}
a__and(x1,x2)	weight: max{x2, x1}
   U41(x1,x2)	weight: max{x2, x1}
#a__U32(x1,x2)	weight: 0
    Usable rules: { 1..62 }
    Removed DPs: #72 #73
Number of SCCs: 1, DPs: 35, edges: 235
	SCC { #5..11 #17 #20 #21 #25 #26 #29 #30 #35..38 #42 #45 #47 #48 #52..54 #60 #66 #67 #70 #71 #74 #75 #77 #78 #82 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: (/ 3 8)
#a__isNatKind(x1)	weight: (/ 3 8)
isNatKind(x1)	weight: 0
a__plus(x1,x2)	weight: max{x2, x1}
   U21(x1,x2)	weight: max{0, x1}
#a__U71(x1,x2,x3)	weight: max{0, (/ 3 4) + x3, (/ 1 2) + x2}
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: x1
#a__U31(x1,x2,x3)	weight: 0
#a__U33(x1)	weight: 0
a__U33(x1)	weight: 0
#a__isNat(x1)	weight: (/ 3 8)
   U71(x1,x2,x3)	weight: max{(/ 3 8) + x3, (/ 1 8) + x2, (/ 3 8) + x1}
   and(x1,x2)	weight: max{x2, x1}
#a__U13(x1)	weight: 0
#a__U51(x1,x2,x3)	weight: max{(/ 3 8) + x3, (/ 1 8) + x2, (/ 1 4) + x1}
#a__x(x1,x2)	weight: max{(/ 1 2) + x2, (/ 3 4) + x1}
a__U22(x1)	weight: x1
#a__U11(x1,x2,x3)	weight: max{0, (/ 3 8) + x1}
a__U31(x1,x2,x3)	weight: 0
a__U51(x1,x2,x3)	weight: max{x3, x2, x1}
  a__x(x1,x2)	weight: max{(/ 1 8) + x2, (/ 3 8) + x1}
   U12(x1,x2)	weight: max{0, x1}
a__U41(x1,x2)	weight: max{x2, (/ 1 8) + x1}
     x(x1,x2)	weight: max{(/ 1 8) + x2, (/ 3 8) + x1}
#a__U12(x1,x2)	weight: 0
#a__U21(x1,x2)	weight: max{0, (/ 3 8) + x1}
#a__U61(x1)	weight: 0
#a__plus(x1,x2)	weight: max{(/ 1 8) + x2, (/ 3 8) + x1}
#mark(x1)	weight: (/ 3 8) + x1
#a__and(x1,x2)	weight: max{(/ 3 8) + x2, (/ 3 8) + x1}
a__U21(x1,x2)	weight: max{0, x1}
a__U32(x1,x2)	weight: 0
  mark(x1)	weight: x1
a__U11(x1,x2,x3)	weight: 0
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
a__U12(x1,x2)	weight: max{0, x1}
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: max{x2, x1}
   U61(x1)	weight: (/ 3 8)
#a__U22(x1)	weight: 0
a__U13(x1)	weight: 0
   U31(x1,x2,x3)	weight: 0
a__U71(x1,x2,x3)	weight: max{(/ 3 8) + x3, (/ 1 8) + x2, (/ 3 8) + x1}
a__U61(x1)	weight: (/ 3 8)
#a__U41(x1,x2)	weight: max{0, (/ 3 8) + x2}
    tt()	weight: 0
a__isNat(x1)	weight: 0
   U13(x1)	weight: 0
a__isNatKind(x1)	weight: 0
   U22(x1)	weight: x1
   U51(x1,x2,x3)	weight: max{x3, x2, x1}
a__and(x1,x2)	weight: max{x2, x1}
   U41(x1,x2)	weight: max{x2, (/ 1 8) + x1}
#a__U32(x1,x2)	weight: 0
    Usable rules: { 1..62 }
    Removed DPs: #6
Number of SCCs: 1, DPs: 34, edges: 208
	SCC { #5 #7..11 #17 #20 #21 #25 #26 #29 #30 #35..38 #42 #45 #47 #48 #52..54 #60 #66 #67 #70 #71 #74 #75 #77 #78 #82 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: 0
#a__isNatKind(x1)	weight: (/ 1 4)
isNatKind(x1)	weight: 0
a__plus(x1,x2)	weight: max{(/ 1 4) + x2, x1}
   U21(x1,x2)	weight: max{0, x1}
#a__U71(x1,x2,x3)	weight: max{0, (/ 1 2) + x3}
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: x1
#a__U31(x1,x2,x3)	weight: 0
#a__U33(x1)	weight: 0
a__U33(x1)	weight: 0
#a__isNat(x1)	weight: (/ 1 4)
   U71(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, (/ 1 4) + x1}
   and(x1,x2)	weight: max{x2, x1}
#a__U13(x1)	weight: 0
#a__U51(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, (/ 1 4) + x1}
#a__x(x1,x2)	weight: max{0, (/ 1 2) + x1}
a__U22(x1)	weight: x1
#a__U11(x1,x2,x3)	weight: max{0, (/ 1 4) + x1}
a__U31(x1,x2,x3)	weight: 0
a__U51(x1,x2,x3)	weight: max{x3, (/ 1 4) + x2, (/ 1 4) + x1}
  a__x(x1,x2)	weight: max{0, (/ 1 4) + x1}
   U12(x1,x2)	weight: max{0, x1}
a__U41(x1,x2)	weight: max{x2, (/ 1 4) + x1}
     x(x1,x2)	weight: max{0, (/ 1 4) + x1}
#a__U12(x1,x2)	weight: 0
#a__U21(x1,x2)	weight: max{0, (/ 1 4) + x1}
#a__U61(x1)	weight: 0
#a__plus(x1,x2)	weight: max{0, (/ 1 4) + x1}
#mark(x1)	weight: (/ 1 4) + x1
#a__and(x1,x2)	weight: max{0, (/ 1 4) + x2}
a__U21(x1,x2)	weight: max{0, x1}
a__U32(x1,x2)	weight: 0
  mark(x1)	weight: x1
a__U11(x1,x2,x3)	weight: 0
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
a__U12(x1,x2)	weight: max{0, x1}
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: max{(/ 1 4) + x2, x1}
   U61(x1)	weight: 0
#a__U22(x1)	weight: 0
a__U13(x1)	weight: 0
   U31(x1,x2,x3)	weight: 0
a__U71(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, (/ 1 4) + x1}
a__U61(x1)	weight: 0
#a__U41(x1,x2)	weight: max{0, (/ 1 4) + x2}
    tt()	weight: 0
a__isNat(x1)	weight: 0
   U13(x1)	weight: 0
a__isNatKind(x1)	weight: 0
   U22(x1)	weight: x1
   U51(x1,x2,x3)	weight: max{x3, (/ 1 4) + x2, (/ 1 4) + x1}
a__and(x1,x2)	weight: max{x2, x1}
   U41(x1,x2)	weight: max{x2, (/ 1 4) + x1}
#a__U32(x1,x2)	weight: 0
    Usable rules: { 1..62 }
    Removed DPs: #71
Number of SCCs: 1, DPs: 33, edges: 183
	SCC { #5 #7..11 #17 #20 #21 #25 #26 #29 #30 #35..38 #42 #45 #47 #48 #52..54 #60 #66 #67 #70 #74 #75 #77 #78 #82 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: (/ 1 8)
#a__isNatKind(x1)	weight: (/ 1 8)
isNatKind(x1)	weight: 0
a__plus(x1,x2)	weight: max{(/ 3 8) + x2, x1}
   U21(x1,x2)	weight: max{0, (/ 1 8) + x1}
#a__U71(x1,x2,x3)	weight: max{0, (/ 1 2) + x3}
   U11(x1,x2,x3)	weight: max{0, (/ 1 8) + x1}
     s(x1)	weight: x1
#a__U31(x1,x2,x3)	weight: 0
#a__U33(x1)	weight: 0
a__U33(x1)	weight: 0
#a__isNat(x1)	weight: (/ 1 8)
   U71(x1,x2,x3)	weight: max{0, (/ 3 8) + x3}
   and(x1,x2)	weight: max{x2, x1}
#a__U13(x1)	weight: 0
#a__U51(x1,x2,x3)	weight: max{(/ 1 8) + x3, (/ 3 8) + x2, (/ 1 8) + x1}
#a__x(x1,x2)	weight: max{0, (/ 1 2) + x1}
a__U22(x1)	weight: x1
#a__U11(x1,x2,x3)	weight: max{0, (/ 1 8) + x1}
a__U31(x1,x2,x3)	weight: 0
a__U51(x1,x2,x3)	weight: max{x3, (/ 3 8) + x2, x1}
  a__x(x1,x2)	weight: max{0, (/ 3 8) + x1}
   U12(x1,x2)	weight: max{0, x1}
a__U41(x1,x2)	weight: max{x2, (/ 1 8) + x1}
     x(x1,x2)	weight: max{0, (/ 3 8) + x1}
#a__U12(x1,x2)	weight: 0
#a__U21(x1,x2)	weight: max{0, (/ 1 8) + x1}
#a__U61(x1)	weight: 0
#a__plus(x1,x2)	weight: max{(/ 3 8) + x2, (/ 1 8) + x1}
#mark(x1)	weight: (/ 1 8) + x1
#a__and(x1,x2)	weight: max{0, (/ 1 8) + x2}
a__U21(x1,x2)	weight: max{0, (/ 1 8) + x1}
a__U32(x1,x2)	weight: 0
  mark(x1)	weight: x1
a__U11(x1,x2,x3)	weight: max{0, (/ 1 8) + x1}
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
a__U12(x1,x2)	weight: max{0, x1}
 isNat(x1)	weight: (/ 1 8)
  plus(x1,x2)	weight: max{(/ 3 8) + x2, x1}
   U61(x1)	weight: (/ 1 8) + x1
#a__U22(x1)	weight: 0
a__U13(x1)	weight: 0
   U31(x1,x2,x3)	weight: 0
a__U71(x1,x2,x3)	weight: max{0, (/ 3 8) + x3}
a__U61(x1)	weight: (/ 1 8) + x1
#a__U41(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 8) + x1}
    tt()	weight: 0
a__isNat(x1)	weight: (/ 1 8)
   U13(x1)	weight: 0
a__isNatKind(x1)	weight: 0
   U22(x1)	weight: x1
   U51(x1,x2,x3)	weight: max{x3, (/ 3 8) + x2, x1}
a__and(x1,x2)	weight: max{x2, x1}
   U41(x1,x2)	weight: max{x2, (/ 1 8) + x1}
#a__U32(x1,x2)	weight: 0
    Usable rules: { 1..62 }
    Removed DPs: #26 #36 #37 #53
Number of SCCs: 2, DPs: 28, edges: 131
	SCC { #74 #77 #78 #82 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
#a__isNatKind(x1)	weight: 0
isNatKind(x1)	weight: (/ 1 8)
a__plus(x1,x2)	weight: (/ 1 8) + x2
   U21(x1,x2)	weight: (/ 9 16)
#a__U71(x1,x2,x3)	weight: (/ 1 8)
   U11(x1,x2,x3)	weight: (/ 9 16) + x1 + x3
     s(x1)	weight: (/ 1 8) + x1
#a__U31(x1,x2,x3)	weight: 0
#a__U33(x1)	weight: 0
a__U33(x1)	weight: (/ 1 16) + x1
#a__isNat(x1)	weight: x1
   U71(x1,x2,x3)	weight: (/ 1 2)
   and(x1,x2)	weight: (/ 3 8)
#a__U13(x1)	weight: 0
#a__U51(x1,x2,x3)	weight: 0
#a__x(x1,x2)	weight: (/ 1 8)
a__U22(x1)	weight: (/ 9 16)
#a__U11(x1,x2,x3)	weight: (/ 1 8) + x2
a__U31(x1,x2,x3)	weight: (/ 3 16) + x1
a__U51(x1,x2,x3)	weight: (/ 9 16) + x1 + x2
  a__x(x1,x2)	weight: (/ 1 16)
   U12(x1,x2)	weight: (/ 5 8)
a__U41(x1,x2)	weight: (/ 3 16)
     x(x1,x2)	weight: (/ 1 8) + x2
#a__U12(x1,x2)	weight: 0
#a__U21(x1,x2)	weight: (/ 1 16) + x2
#a__U61(x1)	weight: 0
#a__plus(x1,x2)	weight: 0
#mark(x1)	weight: 0
#a__and(x1,x2)	weight: 0
a__U21(x1,x2)	weight: (/ 1 2) + x2
a__U32(x1,x2)	weight: (/ 7 16) + x2
  mark(x1)	weight: (/ 3 8)
a__U11(x1,x2,x3)	weight: (/ 1 2)
   U32(x1,x2)	weight: (/ 1 2) + x1
   U33(x1)	weight: (/ 1 8)
a__U12(x1,x2)	weight: (/ 9 16) + x2
 isNat(x1)	weight: (/ 1 2) + x1
  plus(x1,x2)	weight: (/ 3 16) + x1
   U61(x1)	weight: (/ 1 2)
#a__U22(x1)	weight: 0
a__U13(x1)	weight: (/ 3 16) + x1
   U31(x1,x2,x3)	weight: (/ 1 4)
a__U71(x1,x2,x3)	weight: (/ 7 16) + x2 + x3
a__U61(x1)	weight: (/ 7 16)
#a__U41(x1,x2)	weight: 0
    tt()	weight: 0
a__isNat(x1)	weight: (/ 7 16)
   U13(x1)	weight: (/ 1 4)
a__isNatKind(x1)	weight: (/ 1 16) + x1
   U22(x1)	weight: (/ 5 8)
   U51(x1,x2,x3)	weight: (/ 5 8)
a__and(x1,x2)	weight: (/ 5 16)
   U41(x1,x2)	weight: (/ 1 4)
#a__U32(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #74 #77 #78 #82
Number of SCCs: 1, DPs: 24, edges: 125
	SCC { #5 #7..11 #17 #20 #21 #25 #29 #30 #35 #38 #42 #45 #47 #48 #52 #54 #60 #66 #67 #70 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
   |0|()	weight: (/ 1 8)
#a__isNatKind(x1)	weight: (/ 100147 8) + x1
isNatKind(x1)	weight: (/ 100145 8) + x1
a__plus(x1,x2)	weight: max{(/ 1 4) + x2, x1}
   U21(x1,x2)	weight: 0
#a__U71(x1,x2,x3)	weight: max{12519 + x3, (/ 100153 8) + x2, (/ 1 8) + x1}
   U11(x1,x2,x3)	weight: 0
     s(x1)	weight: x1
#a__U31(x1,x2,x3)	weight: 0
#a__U33(x1)	weight: 0
a__U33(x1)	weight: 0
#a__isNat(x1)	weight: (/ 1 8)
   U71(x1,x2,x3)	weight: max{(/ 100149 8) + x3, (/ 50075 4) + x2, (/ 1 4) + x1}
   and(x1,x2)	weight: max{(/ 1 8) + x2, x1}
#a__U13(x1)	weight: 0
#a__U51(x1,x2,x3)	weight: max{0, (/ 3 8) + x3}
#a__x(x1,x2)	weight: max{(/ 100153 8) + x2, 12519 + x1}
a__U22(x1)	weight: x1
#a__U11(x1,x2,x3)	weight: 0
a__U31(x1,x2,x3)	weight: 0
a__U51(x1,x2,x3)	weight: max{0, x3, (/ 1 4) + x2}
  a__x(x1,x2)	weight: max{(/ 50075 4) + x2, (/ 100149 8) + x1}
   U12(x1,x2)	weight: max{0, x1}
a__U41(x1,x2)	weight: max{0, x2}
     x(x1,x2)	weight: max{(/ 50075 4) + x2, (/ 100149 8) + x1}
#a__U12(x1,x2)	weight: 0
#a__U21(x1,x2)	weight: 0
#a__U61(x1)	weight: 0
#a__plus(x1,x2)	weight: max{0, (/ 3 8) + x1}
#mark(x1)	weight: (/ 3 8) + x1
#a__and(x1,x2)	weight: max{(/ 3 8) + x2, (/ 1 8) + x1}
a__U21(x1,x2)	weight: 0
a__U32(x1,x2)	weight: 0
  mark(x1)	weight: x1
a__U11(x1,x2,x3)	weight: 0
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
a__U12(x1,x2)	weight: max{0, x1}
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: max{(/ 1 4) + x2, x1}
   U61(x1)	weight: (/ 3 8) + x1
#a__U22(x1)	weight: 0
a__U13(x1)	weight: 0
   U31(x1,x2,x3)	weight: 0
a__U71(x1,x2,x3)	weight: max{(/ 100149 8) + x3, (/ 50075 4) + x2, (/ 1 4) + x1}
a__U61(x1)	weight: (/ 3 8) + x1
#a__U41(x1,x2)	weight: max{0, (/ 3 8) + x2}
    tt()	weight: 0
a__isNat(x1)	weight: 0
   U13(x1)	weight: 0
a__isNatKind(x1)	weight: (/ 100145 8) + x1
   U22(x1)	weight: x1
   U51(x1,x2,x3)	weight: max{0, x3, (/ 1 4) + x2}
a__and(x1,x2)	weight: max{(/ 1 8) + x2, x1}
   U41(x1,x2)	weight: max{0, x2}
#a__U32(x1,x2)	weight: 0
    Usable rules: { 1..62 }
    Removed DPs: #7 #8 #66
Number of SCCs: 2, DPs: 20, edges: 92
	SCC { #42 #67 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
#a__isNatKind(x1)	weight: x1
isNatKind(x1)	weight: (/ 1 8)
a__plus(x1,x2)	weight: (/ 3 8)
   U21(x1,x2)	weight: 0
#a__U71(x1,x2,x3)	weight: (/ 1 8)
   U11(x1,x2,x3)	weight: x3
     s(x1)	weight: (/ 1 8) + x1
#a__U31(x1,x2,x3)	weight: 0
#a__U33(x1)	weight: 0
a__U33(x1)	weight: x1
#a__isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 1 4) + x2
   and(x1,x2)	weight: (/ 3 8)
#a__U13(x1)	weight: 0
#a__U51(x1,x2,x3)	weight: 0
#a__x(x1,x2)	weight: (/ 1 8)
a__U22(x1)	weight: 0
#a__U11(x1,x2,x3)	weight: (/ 1 4)
a__U31(x1,x2,x3)	weight: 0
a__U51(x1,x2,x3)	weight: (/ 3 8) + x3
  a__x(x1,x2)	weight: (/ 1 8)
   U12(x1,x2)	weight: (/ 1 8)
a__U41(x1,x2)	weight: (/ 3 8)
     x(x1,x2)	weight: (/ 1 4)
#a__U12(x1,x2)	weight: 0
#a__U21(x1,x2)	weight: (/ 1 8)
#a__U61(x1)	weight: 0
#a__plus(x1,x2)	weight: 0
#mark(x1)	weight: 0
#a__and(x1,x2)	weight: 0
a__U21(x1,x2)	weight: 0
a__U32(x1,x2)	weight: x2
  mark(x1)	weight: (/ 3 8)
a__U11(x1,x2,x3)	weight: (/ 1 8)
   U32(x1,x2)	weight: x1
   U33(x1)	weight: 0
a__U12(x1,x2)	weight: (/ 1 8)
 isNat(x1)	weight: (/ 1 8)
  plus(x1,x2)	weight: (/ 1 2) + x1
   U61(x1)	weight: 0
#a__U22(x1)	weight: 0
a__U13(x1)	weight: x1
   U31(x1,x2,x3)	weight: 0
a__U71(x1,x2,x3)	weight: (/ 1 4)
a__U61(x1)	weight: 0
#a__U41(x1,x2)	weight: 0
    tt()	weight: 0
a__isNat(x1)	weight: (/ 1 2) + x1
   U13(x1)	weight: 0
a__isNatKind(x1)	weight: (/ 1 8)
   U22(x1)	weight: 0
   U51(x1,x2,x3)	weight: (/ 3 8)
a__and(x1,x2)	weight: (/ 1 4)
   U41(x1,x2)	weight: (/ 1 8)
#a__U32(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #42 #67
Number of SCCs: 1, DPs: 18, edges: 88
	SCC { #5 #9..11 #17 #21 #25 #29 #30 #35 #38 #45 #47 #48 #52 #54 #60 #70 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
   |0|()	status: []	precedence above: U21 U11 a__U31 U12 a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat a__U13 U31 tt a__isNat U13
#a__isNatKind(x1)	status: []	precedence above:
isNatKind(x1)	status: [x1]	precedence above: #mark a__isNatKind
a__plus(x1,x2)	status: [x1,x2]	precedence above: isNatKind U21 U11 s and #a__U51 a__U22 a__U31 a__U51 U12 a__U41 #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 #a__U41 tt a__isNat U13 a__isNatKind U22 U51 a__and U41
   U21(x1,x2)	status: []	precedence above: U11 a__U31 U12 a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat a__U13 U31 tt a__isNat U13
#a__U71(x1,x2,x3)	status: [x3,x2,x1]	precedence above: |0| isNatKind a__plus U21 U11 s U71 and #a__U51 #a__x a__U22 a__U31 a__U51 a__x U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus U61 a__U13 U31 a__U71 a__U61 #a__U41 tt a__isNat U13 a__isNatKind U22 U51 a__and U41
   U11(x1,x2,x3)	status: []	precedence above: U21 a__U31 U12 a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat a__U13 U31 tt a__isNat U13
     s(x1)	status: [x1]	precedence above: isNatKind U21 U11 and #a__U51 a__U22 a__U31 U12 a__U41 #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat a__U13 U31 #a__U41 tt a__isNat U13 a__isNatKind U22 a__and U41
#a__U31(x1,x2,x3)	status: [x3,x2]	precedence above:
#a__U33(x1)	status: []	precedence above:
a__U33(x1)	status: x1
#a__isNat(x1)	status: []	precedence above:
   U71(x1,x2,x3)	status: [x3,x2,x1]	precedence above: |0| isNatKind a__plus U21 #a__U71 U11 s and #a__U51 #a__x a__U22 a__U31 a__U51 a__x U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus U61 a__U13 U31 a__U71 a__U61 #a__U41 tt a__isNat U13 a__isNatKind U22 U51 a__and U41
   and(x1,x2)	status: [x1,x2]	precedence above: isNatKind #a__U51 a__U22 U12 a__U41 #a__plus #mark mark U33 #a__U41 a__isNatKind a__and U41
#a__U13(x1)	status: []	precedence above:
#a__U51(x1,x2,x3)	status: [x2,x3,x1]	precedence above: isNatKind and a__U22 U12 a__U41 #a__plus #mark mark U33 #a__U41 a__isNatKind a__and U41
#a__x(x1,x2)	status: [x1,x2]	precedence above: |0| isNatKind a__plus U21 #a__U71 U11 s U71 and #a__U51 a__U22 a__U31 a__U51 a__x U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus U61 a__U13 U31 a__U71 a__U61 #a__U41 tt a__isNat U13 a__isNatKind U22 U51 a__and U41
a__U22(x1)	status: x1
#a__U11(x1,x2,x3)	status: [x2,x3]	precedence above:
a__U31(x1,x2,x3)	status: []	precedence above: U21 U11 U12 a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat a__U13 U31 tt a__isNat U13
a__U51(x1,x2,x3)	status: [x3,x2,x1]	precedence above: isNatKind a__plus U21 U11 s and #a__U51 a__U22 a__U31 U12 a__U41 #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 #a__U41 tt a__isNat U13 a__isNatKind U22 U51 a__and U41
  a__x(x1,x2)	status: [x1,x2]	precedence above: |0| isNatKind a__plus U21 #a__U71 U11 s U71 and #a__U51 #a__x a__U22 a__U31 a__U51 U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus U61 a__U13 U31 a__U71 a__U61 #a__U41 tt a__isNat U13 a__isNatKind U22 U51 a__and U41
   U12(x1,x2)	status: x1
a__U41(x1,x2)	status: [x1,x2]	precedence above: isNatKind U12 #mark mark U33 #a__U41 a__isNatKind U41
     x(x1,x2)	status: [x1,x2]	precedence above: |0| isNatKind a__plus U21 #a__U71 U11 s U71 and #a__U51 #a__x a__U22 a__U31 a__U51 a__x U12 a__U41 #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus U61 a__U13 U31 a__U71 a__U61 #a__U41 tt a__isNat U13 a__isNatKind U22 U51 a__and U41
#a__U12(x1,x2)	status: [x1,x2]	precedence above:
#a__U21(x1,x2)	status: []	precedence above:
#a__U61(x1)	status: []	precedence above:
#a__plus(x1,x2)	status: [x2,x1]	precedence above: isNatKind and #a__U51 a__U22 U12 a__U41 #mark mark U33 #a__U41 a__isNatKind a__and U41
#mark(x1)	status: [x1]	precedence above:
#a__and(x1,x2)	status: [x1]	precedence above:
a__U21(x1,x2)	status: []	precedence above: U21 U11 a__U31 U12 a__U32 mark a__U11 U32 U33 a__U12 isNat a__U13 U31 tt a__isNat U13
a__U32(x1,x2)	status: []	precedence above: U21 U11 a__U31 U12 a__U21 mark a__U11 U32 U33 a__U12 isNat a__U13 U31 tt a__isNat U13
  mark(x1)	status: x1
a__U11(x1,x2,x3)	status: []	precedence above: U21 U11 a__U31 U12 a__U21 a__U32 mark U32 U33 a__U12 isNat a__U13 U31 tt a__isNat U13
   U32(x1,x2)	status: []	precedence above: U21 U11 a__U31 U12 a__U21 a__U32 mark a__U11 U33 a__U12 isNat a__U13 U31 tt a__isNat U13
   U33(x1)	status: x1
a__U12(x1,x2)	status: x1
 isNat(x1)	status: []	precedence above: U21 U11 a__U31 U12 a__U21 a__U32 mark a__U11 U32 U33 a__U12 a__U13 U31 tt a__isNat U13
  plus(x1,x2)	status: [x1,x2]	precedence above: isNatKind a__plus U21 U11 s and #a__U51 a__U22 a__U31 a__U51 U12 a__U41 #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat a__U13 U31 #a__U41 tt a__isNat U13 a__isNatKind U22 U51 a__and U41
   U61(x1)	status: [x1]	precedence above: |0| U21 U11 a__U31 U12 a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat a__U13 U31 a__U61 tt a__isNat U13
#a__U22(x1)	status: []	precedence above:
a__U13(x1)	status: []	precedence above: tt U13
   U31(x1,x2,x3)	status: []	precedence above: U21 U11 a__U31 U12 a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat a__U13 tt a__isNat U13
a__U71(x1,x2,x3)	status: [x3,x2,x1]	precedence above: |0| isNatKind a__plus U21 #a__U71 U11 s U71 and #a__U51 #a__x a__U22 a__U31 a__U51 a__x U12 a__U41 x #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus U61 a__U13 U31 a__U61 #a__U41 tt a__isNat U13 a__isNatKind U22 U51 a__and U41
a__U61(x1)	status: [x1]	precedence above: |0| U21 U11 a__U31 U12 a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat U61 a__U13 U31 tt a__isNat U13
#a__U41(x1,x2)	status: [x1,x2]	precedence above: isNatKind U12 a__U41 #mark mark U33 a__isNatKind U41
    tt()	status: []	precedence above: a__U13 U13
a__isNat(x1)	status: []	precedence above: U21 U11 a__U31 U12 a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat a__U13 U31 tt U13
   U13(x1)	status: []	precedence above: a__U13 tt
a__isNatKind(x1)	status: [x1]	precedence above: isNatKind #mark
   U22(x1)	status: x1
   U51(x1,x2,x3)	status: [x3,x2,x1]	precedence above: isNatKind a__plus U21 U11 s and #a__U51 a__U22 a__U31 a__U51 U12 a__U41 #a__plus #mark a__U21 a__U32 mark a__U11 U32 U33 a__U12 isNat plus a__U13 U31 #a__U41 tt a__isNat U13 a__isNatKind U22 a__and U41
a__and(x1,x2)	status: [x1,x2]	precedence above: isNatKind and #a__U51 a__U22 U12 a__U41 #a__plus #mark mark U33 #a__U41 a__isNatKind U41
   U41(x1,x2)	status: [x1,x2]	precedence above: isNatKind U12 a__U41 #mark mark U33 #a__U41 a__isNatKind
#a__U32(x1,x2)	status: [x1]	precedence above:
    Usable rules: { 1..62 }
    Removed DPs: #5 #9..11 #17 #21 #25 #29 #30 #38 #45 #47 #48 #52 #54 #70
Number of SCCs: 1, DPs: 2, edges: 4
	SCC { #35 #60 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
#a__isNatKind(x1)	weight: 0
isNatKind(x1)	weight: (/ 1 4)
a__plus(x1,x2)	weight: (/ 7 16)
   U21(x1,x2)	weight: (/ 3 8)
#a__U71(x1,x2,x3)	weight: (/ 1 16)
   U11(x1,x2,x3)	weight: (/ 13 16) + x1
     s(x1)	weight: (/ 1 4)
#a__U31(x1,x2,x3)	weight: 0
#a__U33(x1)	weight: 0
a__U33(x1)	weight: (/ 5 16) + x1
#a__isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: (/ 7 16) + x2
   and(x1,x2)	weight: (/ 1 8)
#a__U13(x1)	weight: 0
#a__U51(x1,x2,x3)	weight: (/ 1 16)
#a__x(x1,x2)	weight: (/ 1 16)
a__U22(x1)	weight: (/ 3 8)
#a__U11(x1,x2,x3)	weight: (/ 1 8)
a__U31(x1,x2,x3)	weight: (/ 3 8)
a__U51(x1,x2,x3)	weight: (/ 3 16)
  a__x(x1,x2)	weight: (/ 1 16) + x2
   U12(x1,x2)	weight: (/ 11 16) + x1
a__U41(x1,x2)	weight: (/ 1 2)
     x(x1,x2)	weight: (/ 1 8)
#a__U12(x1,x2)	weight: 0
#a__U21(x1,x2)	weight: (/ 1 16)
#a__U61(x1)	weight: 0
#a__plus(x1,x2)	weight: 0
#mark(x1)	weight: (/ 1 16) + x1
#a__and(x1,x2)	weight: 0
a__U21(x1,x2)	weight: (/ 5 16) + x1 + x2
a__U32(x1,x2)	weight: (/ 7 16)
  mark(x1)	weight: (/ 1 8)
a__U11(x1,x2,x3)	weight: (/ 3 4)
   U32(x1,x2)	weight: (/ 1 2) + x1 + x2
   U33(x1)	weight: (/ 3 8)
a__U12(x1,x2)	weight: (/ 5 8) + x1 + x2
 isNat(x1)	weight: (/ 1 4)
  plus(x1,x2)	weight: (/ 1 2)
   U61(x1)	weight: (/ 1 4) + x1
#a__U22(x1)	weight: 0
a__U13(x1)	weight: (/ 11 16)
   U31(x1,x2,x3)	weight: (/ 7 16) + x1 + x2
a__U71(x1,x2,x3)	weight: (/ 3 8)
a__U61(x1)	weight: (/ 3 16)
#a__U41(x1,x2)	weight: (/ 1 16)
    tt()	weight: 0
a__isNat(x1)	weight: (/ 3 16) + x1
   U13(x1)	weight: (/ 3 4)
a__isNatKind(x1)	weight: (/ 3 16)
   U22(x1)	weight: (/ 7 16) + x1
   U51(x1,x2,x3)	weight: (/ 1 4)
a__and(x1,x2)	weight: (/ 1 16)
   U41(x1,x2)	weight: (/ 9 16)
#a__U32(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #35 #60
Number of SCCs: 0, DPs: 0, edges: 0
YES