Input TRS:
    1: active(U11(tt(),V2)) -> mark(U12(isNat(V2)))
    2: active(U12(tt())) -> mark(tt())
    3: active(U21(tt())) -> mark(tt())
    4: active(U31(tt(),V2)) -> mark(U32(isNat(V2)))
    5: active(U32(tt())) -> mark(tt())
    6: active(U41(tt(),N)) -> mark(N)
    7: active(U51(tt(),M,N)) -> mark(U52(isNat(N),M,N))
    8: active(U52(tt(),M,N)) -> mark(s(plus(N,M)))
    9: active(U61(tt())) -> mark(0())
    10: active(U71(tt(),M,N)) -> mark(U72(isNat(N),M,N))
    11: active(U72(tt(),M,N)) -> mark(plus(x(N,M),N))
    12: active(isNat(0())) -> mark(tt())
    13: active(isNat(plus(V1,V2))) -> mark(U11(isNat(V1),V2))
    14: active(isNat(s(V1))) -> mark(U21(isNat(V1)))
    15: active(isNat(x(V1,V2))) -> mark(U31(isNat(V1),V2))
    16: active(plus(N,0())) -> mark(U41(isNat(N),N))
    17: active(plus(N,s(M))) -> mark(U51(isNat(M),M,N))
    18: active(x(N,0())) -> mark(U61(isNat(N)))
    19: active(x(N,s(M))) -> mark(U71(isNat(M),M,N))
    20: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
    21: mark(tt()) -> active(tt())
    22: mark(U12(X)) -> active(U12(mark(X)))
    23: mark(isNat(X)) -> active(isNat(X))
    24: mark(U21(X)) -> active(U21(mark(X)))
    25: mark(U31(X1,X2)) -> active(U31(mark(X1),X2))
    26: mark(U32(X)) -> active(U32(mark(X)))
    27: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
    28: mark(U51(X1,X2,X3)) -> active(U51(mark(X1),X2,X3))
    29: mark(U52(X1,X2,X3)) -> active(U52(mark(X1),X2,X3))
    30: mark(s(X)) -> active(s(mark(X)))
    31: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2)))
    32: mark(U61(X)) -> active(U61(mark(X)))
    33: mark(0()) -> active(0())
    34: mark(U71(X1,X2,X3)) -> active(U71(mark(X1),X2,X3))
    35: mark(U72(X1,X2,X3)) -> active(U72(mark(X1),X2,X3))
    36: mark(x(X1,X2)) -> active(x(mark(X1),mark(X2)))
    37: U11(mark(X1),X2) -> U11(X1,X2)
    38: U11(X1,mark(X2)) -> U11(X1,X2)
    39: U11(active(X1),X2) -> U11(X1,X2)
    40: U11(X1,active(X2)) -> U11(X1,X2)
    41: U12(mark(X)) -> U12(X)
    42: U12(active(X)) -> U12(X)
    43: isNat(mark(X)) -> isNat(X)
    44: isNat(active(X)) -> isNat(X)
    45: U21(mark(X)) -> U21(X)
    46: U21(active(X)) -> U21(X)
    47: U31(mark(X1),X2) -> U31(X1,X2)
    48: U31(X1,mark(X2)) -> U31(X1,X2)
    49: U31(active(X1),X2) -> U31(X1,X2)
    50: U31(X1,active(X2)) -> U31(X1,X2)
    51: U32(mark(X)) -> U32(X)
    52: U32(active(X)) -> U32(X)
    53: U41(mark(X1),X2) -> U41(X1,X2)
    54: U41(X1,mark(X2)) -> U41(X1,X2)
    55: U41(active(X1),X2) -> U41(X1,X2)
    56: U41(X1,active(X2)) -> U41(X1,X2)
    57: U51(mark(X1),X2,X3) -> U51(X1,X2,X3)
    58: U51(X1,mark(X2),X3) -> U51(X1,X2,X3)
    59: U51(X1,X2,mark(X3)) -> U51(X1,X2,X3)
    60: U51(active(X1),X2,X3) -> U51(X1,X2,X3)
    61: U51(X1,active(X2),X3) -> U51(X1,X2,X3)
    62: U51(X1,X2,active(X3)) -> U51(X1,X2,X3)
    63: U52(mark(X1),X2,X3) -> U52(X1,X2,X3)
    64: U52(X1,mark(X2),X3) -> U52(X1,X2,X3)
    65: U52(X1,X2,mark(X3)) -> U52(X1,X2,X3)
    66: U52(active(X1),X2,X3) -> U52(X1,X2,X3)
    67: U52(X1,active(X2),X3) -> U52(X1,X2,X3)
    68: U52(X1,X2,active(X3)) -> U52(X1,X2,X3)
    69: s(mark(X)) -> s(X)
    70: s(active(X)) -> s(X)
    71: plus(mark(X1),X2) -> plus(X1,X2)
    72: plus(X1,mark(X2)) -> plus(X1,X2)
    73: plus(active(X1),X2) -> plus(X1,X2)
    74: plus(X1,active(X2)) -> plus(X1,X2)
    75: U61(mark(X)) -> U61(X)
    76: U61(active(X)) -> U61(X)
    77: U71(mark(X1),X2,X3) -> U71(X1,X2,X3)
    78: U71(X1,mark(X2),X3) -> U71(X1,X2,X3)
    79: U71(X1,X2,mark(X3)) -> U71(X1,X2,X3)
    80: U71(active(X1),X2,X3) -> U71(X1,X2,X3)
    81: U71(X1,active(X2),X3) -> U71(X1,X2,X3)
    82: U71(X1,X2,active(X3)) -> U71(X1,X2,X3)
    83: U72(mark(X1),X2,X3) -> U72(X1,X2,X3)
    84: U72(X1,mark(X2),X3) -> U72(X1,X2,X3)
    85: U72(X1,X2,mark(X3)) -> U72(X1,X2,X3)
    86: U72(active(X1),X2,X3) -> U72(X1,X2,X3)
    87: U72(X1,active(X2),X3) -> U72(X1,X2,X3)
    88: U72(X1,X2,active(X3)) -> U72(X1,X2,X3)
    89: x(mark(X1),X2) -> x(X1,X2)
    90: x(X1,mark(X2)) -> x(X1,X2)
    91: x(active(X1),X2) -> x(X1,X2)
    92: x(X1,active(X2)) -> x(X1,X2)
Number of strict rules: 92
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(U12(tt())) -> #mark(tt())
   #2: #U72(active(X1),X2,X3) -> #U72(X1,X2,X3)
   #3: #isNat(mark(X)) -> #isNat(X)
   #4: #mark(U52(X1,X2,X3)) -> #active(U52(mark(X1),X2,X3))
   #5: #mark(U52(X1,X2,X3)) -> #U52(mark(X1),X2,X3)
   #6: #mark(U52(X1,X2,X3)) -> #mark(X1)
   #7: #mark(U72(X1,X2,X3)) -> #active(U72(mark(X1),X2,X3))
   #8: #mark(U72(X1,X2,X3)) -> #U72(mark(X1),X2,X3)
   #9: #mark(U72(X1,X2,X3)) -> #mark(X1)
   #10: #U72(mark(X1),X2,X3) -> #U72(X1,X2,X3)
   #11: #U52(active(X1),X2,X3) -> #U52(X1,X2,X3)
   #12: #U21(active(X)) -> #U21(X)
   #13: #U12(active(X)) -> #U12(X)
   #14: #U12(mark(X)) -> #U12(X)
   #15: #U11(mark(X1),X2) -> #U11(X1,X2)
   #16: #x(active(X1),X2) -> #x(X1,X2)
   #17: #plus(active(X1),X2) -> #plus(X1,X2)
   #18: #U31(mark(X1),X2) -> #U31(X1,X2)
   #19: #U41(mark(X1),X2) -> #U41(X1,X2)
   #20: #plus(mark(X1),X2) -> #plus(X1,X2)
   #21: #U31(X1,mark(X2)) -> #U31(X1,X2)
   #22: #U61(mark(X)) -> #U61(X)
   #23: #plus(X1,active(X2)) -> #plus(X1,X2)
   #24: #U51(X1,mark(X2),X3) -> #U51(X1,X2,X3)
   #25: #U51(X1,active(X2),X3) -> #U51(X1,X2,X3)
   #26: #U11(X1,mark(X2)) -> #U11(X1,X2)
   #27: #active(U41(tt(),N)) -> #mark(N)
   #28: #U51(X1,X2,mark(X3)) -> #U51(X1,X2,X3)
   #29: #U41(active(X1),X2) -> #U41(X1,X2)
   #30: #U52(X1,active(X2),X3) -> #U52(X1,X2,X3)
   #31: #U11(X1,active(X2)) -> #U11(X1,X2)
   #32: #x(X1,mark(X2)) -> #x(X1,X2)
   #33: #U32(mark(X)) -> #U32(X)
   #34: #active(isNat(plus(V1,V2))) -> #mark(U11(isNat(V1),V2))
   #35: #active(isNat(plus(V1,V2))) -> #U11(isNat(V1),V2)
   #36: #active(isNat(plus(V1,V2))) -> #isNat(V1)
   #37: #active(U61(tt())) -> #mark(0())
   #38: #active(U72(tt(),M,N)) -> #mark(plus(x(N,M),N))
   #39: #active(U72(tt(),M,N)) -> #plus(x(N,M),N)
   #40: #active(U72(tt(),M,N)) -> #x(N,M)
   #41: #U51(mark(X1),X2,X3) -> #U51(X1,X2,X3)
   #42: #U61(active(X)) -> #U61(X)
   #43: #mark(U21(X)) -> #active(U21(mark(X)))
   #44: #mark(U21(X)) -> #U21(mark(X))
   #45: #mark(U21(X)) -> #mark(X)
   #46: #s(active(X)) -> #s(X)
   #47: #mark(isNat(X)) -> #active(isNat(X))
   #48: #U71(X1,active(X2),X3) -> #U71(X1,X2,X3)
   #49: #U71(X1,mark(X2),X3) -> #U71(X1,X2,X3)
   #50: #U21(mark(X)) -> #U21(X)
   #51: #s(mark(X)) -> #s(X)
   #52: #active(isNat(0())) -> #mark(tt())
   #53: #mark(plus(X1,X2)) -> #active(plus(mark(X1),mark(X2)))
   #54: #mark(plus(X1,X2)) -> #plus(mark(X1),mark(X2))
   #55: #mark(plus(X1,X2)) -> #mark(X1)
   #56: #mark(plus(X1,X2)) -> #mark(X2)
   #57: #U71(X1,X2,mark(X3)) -> #U71(X1,X2,X3)
   #58: #U41(X1,active(X2)) -> #U41(X1,X2)
   #59: #x(mark(X1),X2) -> #x(X1,X2)
   #60: #U71(X1,X2,active(X3)) -> #U71(X1,X2,X3)
   #61: #active(isNat(s(V1))) -> #mark(U21(isNat(V1)))
   #62: #active(isNat(s(V1))) -> #U21(isNat(V1))
   #63: #active(isNat(s(V1))) -> #isNat(V1)
   #64: #U51(X1,X2,active(X3)) -> #U51(X1,X2,X3)
   #65: #mark(s(X)) -> #active(s(mark(X)))
   #66: #mark(s(X)) -> #s(mark(X))
   #67: #mark(s(X)) -> #mark(X)
   #68: #U32(active(X)) -> #U32(X)
   #69: #U31(active(X1),X2) -> #U31(X1,X2)
   #70: #mark(U31(X1,X2)) -> #active(U31(mark(X1),X2))
   #71: #mark(U31(X1,X2)) -> #U31(mark(X1),X2)
   #72: #mark(U31(X1,X2)) -> #mark(X1)
   #73: #mark(U11(X1,X2)) -> #active(U11(mark(X1),X2))
   #74: #mark(U11(X1,X2)) -> #U11(mark(X1),X2)
   #75: #mark(U11(X1,X2)) -> #mark(X1)
   #76: #U72(X1,X2,active(X3)) -> #U72(X1,X2,X3)
   #77: #active(U51(tt(),M,N)) -> #mark(U52(isNat(N),M,N))
   #78: #active(U51(tt(),M,N)) -> #U52(isNat(N),M,N)
   #79: #active(U51(tt(),M,N)) -> #isNat(N)
   #80: #U11(active(X1),X2) -> #U11(X1,X2)
   #81: #active(U71(tt(),M,N)) -> #mark(U72(isNat(N),M,N))
   #82: #active(U71(tt(),M,N)) -> #U72(isNat(N),M,N)
   #83: #active(U71(tt(),M,N)) -> #isNat(N)
   #84: #x(X1,active(X2)) -> #x(X1,X2)
   #85: #U52(X1,mark(X2),X3) -> #U52(X1,X2,X3)
   #86: #mark(0()) -> #active(0())
   #87: #plus(X1,mark(X2)) -> #plus(X1,X2)
   #88: #active(U32(tt())) -> #mark(tt())
   #89: #isNat(active(X)) -> #isNat(X)
   #90: #U52(X1,X2,mark(X3)) -> #U52(X1,X2,X3)
   #91: #mark(U51(X1,X2,X3)) -> #active(U51(mark(X1),X2,X3))
   #92: #mark(U51(X1,X2,X3)) -> #U51(mark(X1),X2,X3)
   #93: #mark(U51(X1,X2,X3)) -> #mark(X1)
   #94: #mark(U12(X)) -> #active(U12(mark(X)))
   #95: #mark(U12(X)) -> #U12(mark(X))
   #96: #mark(U12(X)) -> #mark(X)
   #97: #mark(U71(X1,X2,X3)) -> #active(U71(mark(X1),X2,X3))
   #98: #mark(U71(X1,X2,X3)) -> #U71(mark(X1),X2,X3)
   #99: #mark(U71(X1,X2,X3)) -> #mark(X1)
   #100: #U72(X1,mark(X2),X3) -> #U72(X1,X2,X3)
   #101: #U72(X1,active(X2),X3) -> #U72(X1,X2,X3)
   #102: #mark(U41(X1,X2)) -> #active(U41(mark(X1),X2))
   #103: #mark(U41(X1,X2)) -> #U41(mark(X1),X2)
   #104: #mark(U41(X1,X2)) -> #mark(X1)
   #105: #U51(active(X1),X2,X3) -> #U51(X1,X2,X3)
   #106: #active(plus(N,s(M))) -> #mark(U51(isNat(M),M,N))
   #107: #active(plus(N,s(M))) -> #U51(isNat(M),M,N)
   #108: #active(plus(N,s(M))) -> #isNat(M)
   #109: #mark(U61(X)) -> #active(U61(mark(X)))
   #110: #mark(U61(X)) -> #U61(mark(X))
   #111: #mark(U61(X)) -> #mark(X)
   #112: #active(x(N,s(M))) -> #mark(U71(isNat(M),M,N))
   #113: #active(x(N,s(M))) -> #U71(isNat(M),M,N)
   #114: #active(x(N,s(M))) -> #isNat(M)
   #115: #U52(mark(X1),X2,X3) -> #U52(X1,X2,X3)
   #116: #mark(U32(X)) -> #active(U32(mark(X)))
   #117: #mark(U32(X)) -> #U32(mark(X))
   #118: #mark(U32(X)) -> #mark(X)
   #119: #U72(X1,X2,mark(X3)) -> #U72(X1,X2,X3)
   #120: #U52(X1,X2,active(X3)) -> #U52(X1,X2,X3)
   #121: #mark(x(X1,X2)) -> #active(x(mark(X1),mark(X2)))
   #122: #mark(x(X1,X2)) -> #x(mark(X1),mark(X2))
   #123: #mark(x(X1,X2)) -> #mark(X1)
   #124: #mark(x(X1,X2)) -> #mark(X2)
   #125: #mark(tt()) -> #active(tt())
   #126: #active(plus(N,0())) -> #mark(U41(isNat(N),N))
   #127: #active(plus(N,0())) -> #U41(isNat(N),N)
   #128: #active(plus(N,0())) -> #isNat(N)
   #129: #active(U21(tt())) -> #mark(tt())
   #130: #U71(mark(X1),X2,X3) -> #U71(X1,X2,X3)
   #131: #active(U11(tt(),V2)) -> #mark(U12(isNat(V2)))
   #132: #active(U11(tt(),V2)) -> #U12(isNat(V2))
   #133: #active(U11(tt(),V2)) -> #isNat(V2)
   #134: #U41(X1,mark(X2)) -> #U41(X1,X2)
   #135: #active(U52(tt(),M,N)) -> #mark(s(plus(N,M)))
   #136: #active(U52(tt(),M,N)) -> #s(plus(N,M))
   #137: #active(U52(tt(),M,N)) -> #plus(N,M)
   #138: #active(isNat(x(V1,V2))) -> #mark(U31(isNat(V1),V2))
   #139: #active(isNat(x(V1,V2))) -> #U31(isNat(V1),V2)
   #140: #active(isNat(x(V1,V2))) -> #isNat(V1)
   #141: #active(U31(tt(),V2)) -> #mark(U32(isNat(V2)))
   #142: #active(U31(tt(),V2)) -> #U32(isNat(V2))
   #143: #active(U31(tt(),V2)) -> #isNat(V2)
   #144: #U71(active(X1),X2,X3) -> #U71(X1,X2,X3)
   #145: #U31(X1,active(X2)) -> #U31(X1,X2)
   #146: #active(x(N,0())) -> #mark(U61(isNat(N)))
   #147: #active(x(N,0())) -> #U61(isNat(N))
   #148: #active(x(N,0())) -> #isNat(N)
Number of SCCs: 16, DPs: 96, edges: 726
	SCC { #3 #89 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: x1
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #3 #89
Number of SCCs: 15, DPs: 94, edges: 722
	SCC { #33 #68 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: x1
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #33 #68
Number of SCCs: 14, DPs: 92, edges: 718
	SCC { #22 #42 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #22 #42
Number of SCCs: 13, DPs: 90, edges: 714
	SCC { #13 #14 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: x1
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #13 #14
Number of SCCs: 12, DPs: 88, edges: 710
	SCC { #46 #51 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: x1
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #46 #51
Number of SCCs: 11, DPs: 86, edges: 706
	SCC { #12 #50 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: x1
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #12 #50
Number of SCCs: 10, DPs: 84, edges: 702
	SCC { #17 #20 #23 #87 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: x2
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #23 #87
Number of SCCs: 10, DPs: 82, edges: 690
	SCC { #17 #20 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: x1
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #17 #20
Number of SCCs: 9, DPs: 80, edges: 686
	SCC { #16 #32 #59 #84 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: x1
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #16 #59
Number of SCCs: 10, DPs: 78, edges: 674
	SCC { #32 #84 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: x2
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #32 #84
Number of SCCs: 9, DPs: 76, edges: 670
	SCC { #19 #29 #58 #134 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: x2
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #58 #134
Number of SCCs: 10, DPs: 74, edges: 658
	SCC { #19 #29 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: x1
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #19 #29
Number of SCCs: 9, DPs: 72, edges: 654
	SCC { #15 #26 #31 #80 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: x1
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #15 #80
Number of SCCs: 10, DPs: 70, edges: 642
	SCC { #26 #31 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: x2
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #26 #31
Number of SCCs: 9, DPs: 68, edges: 638
	SCC { #18 #21 #69 #145 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: x1
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #18 #69
Number of SCCs: 10, DPs: 66, edges: 626
	SCC { #21 #145 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: x2
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #21 #145
Number of SCCs: 9, DPs: 64, edges: 622
	SCC { #2 #10 #76 #100 #101 #119 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: x2 + x3
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #76 #100 #101 #119
Number of SCCs: 10, DPs: 60, edges: 590
	SCC { #2 #10 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: x1
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #2 #10
Number of SCCs: 9, DPs: 58, edges: 586
	SCC { #48 #49 #57 #60 #130 #144 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: x1 + x3
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #57 #60 #130 #144
Number of SCCs: 10, DPs: 54, edges: 554
	SCC { #48 #49 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: x2
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #48 #49
Number of SCCs: 9, DPs: 52, edges: 550
	SCC { #24 #25 #28 #41 #64 #105 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: x2 + x3
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #24 #25 #28 #64
Number of SCCs: 10, DPs: 48, edges: 518
	SCC { #41 #105 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: x1
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #41 #105
Number of SCCs: 9, DPs: 46, edges: 514
	SCC { #11 #30 #85 #90 #115 #120 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: x2 + x3
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #30 #85 #90 #120
Number of SCCs: 10, DPs: 42, edges: 482
	SCC { #11 #115 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: x1
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   U32(x1)	weight: 0
 isNat(x1)	weight: 0
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: 0
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #11 #115
Number of SCCs: 9, DPs: 40, edges: 478
	SCC { #4 #6 #7 #9 #27 #34 #38 #45 #47 #53 #55 #56 #61 #67 #70 #72 #73 #75 #77 #81 #91 #93 #96 #97 #99 #102 #104 #106 #111 #112 #118 #121 #123 #124 #126 #131 #135 #138 #141 #146 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: x1
   U11(x1,x2)	weight: max{0, x1}
     s(x1)	weight: x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: max{(/ 30879 4) + x3, (/ 30879 2) + x2, 7720 + x1}
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: max{(/ 30879 4) + x3, (/ 30879 2) + x2, (/ 1 4) + x1}
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: x1
     x(x1,x2)	weight: max{(/ 30879 2) + x2, (/ 30879 4) + x1}
 #U12(x1)	weight: 0
#mark(x1)	weight: x1
     0()	weight: (/ 1 4)
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: x1
   U32(x1)	weight: x1
 isNat(x1)	weight: (/ 30877 4)
   U52(x1,x2,x3)	weight: max{x3, (/ 30879 4) + x2, (/ 1 2) + x1}
  plus(x1,x2)	weight: max{(/ 30879 4) + x2, x1}
   U61(x1)	weight: (/ 1 4) + x1
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: x1
   U31(x1,x2)	weight: max{0, x1}
 #U41(x1,x2)	weight: 0
#active(x1)	weight: x1
 #U21(x1)	weight: 0
    tt()	weight: (/ 30877 4)
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: max{x3, (/ 30879 4) + x2, (/ 1 4) + x1}
   U41(x1,x2)	weight: max{x2, (/ 3 4) + x1}
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { 1..92 }
    Removed DPs: #6 #9 #56 #93 #99 #104 #111 #123 #124 #146
Number of SCCs: 10, DPs: 30, edges: 164
	SCC { #4 #7 #27 #34 #38 #45 #47 #53 #55 #61 #67 #70 #72 #73 #75 #77 #81 #91 #96 #97 #102 #106 #112 #118 #121 #126 #131 #135 #138 #141 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: x1
   U11(x1,x2)	weight: max{(/ 1 4) + x2, x1}
     s(x1)	weight: x1
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 7 16) + x2}
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: max{0, (/ 3 8) + x3, (/ 7 16) + x2}
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: (/ 1 16) + x1
     x(x1,x2)	weight: max{(/ 7 16) + x2, (/ 3 8) + x1}
 #U12(x1)	weight: 0
#mark(x1)	weight: x1
     0()	weight: (/ 3 8)
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: x1
   U32(x1)	weight: (/ 1 4) + x1
 isNat(x1)	weight: (/ 1 16) + x1
   U52(x1,x2,x3)	weight: max{0, x3, (/ 3 16) + x2}
  plus(x1,x2)	weight: max{(/ 3 16) + x2, x1}
   U61(x1)	weight: (/ 3 8)
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: x1
   U31(x1,x2)	weight: max{(/ 3 8) + x2, (/ 1 16) + x1}
 #U41(x1,x2)	weight: 0
#active(x1)	weight: x1
 #U21(x1)	weight: 0
    tt()	weight: (/ 3 16)
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: max{x3, (/ 3 16) + x2, (/ 1 16) + x1}
   U41(x1,x2)	weight: max{0, x2}
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { 1..92 }
    Removed DPs: #72 #96 #118 #131 #138 #141
Number of SCCs: 10, DPs: 22, edges: 80
	SCC { #4 #7 #27 #34 #38 #45 #47 #53 #55 #61 #67 #75 #77 #81 #91 #97 #102 #106 #112 #121 #126 #135 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
 #U72(x1,x2,x3)	status: [x3,x2,x1]	precedence above:
 #U32(x1)	status: []	precedence above:
   U21(x1)	status: x1
   U11(x1,x2)	status: x1
     s(x1)	status: [x1]	precedence above: U32 isNat U31 tt
#isNat(x1)	status: []	precedence above:
   U71(x1,x2,x3)	status: [x2,x3,x1]	precedence above: U21 s U72 x #mark mark U32 isNat U52 plus U31 tt U51 U41
#plus(x1,x2)	status: [x2,x1]	precedence above:
   U72(x1,x2,x3)	status: [x2,x3,x1]	precedence above: U21 s U71 x #mark mark U32 isNat U52 plus U31 tt U51 U41
 #U52(x1,x2,x3)	status: [x3]	precedence above:
   U12(x1)	status: x1
     x(x1,x2)	status: [x2,x1]	precedence above: U21 s U71 U72 #mark mark U32 isNat U52 plus U31 tt U51 U41
 #U12(x1)	status: []	precedence above:
#mark(x1)	status: x1
     0()	status: []	precedence above: U61
   #x(x1,x2)	status: [x1,x2]	precedence above:
   #s(x1)	status: []	precedence above:
  mark(x1)	status: x1
   U32(x1)	status: []	precedence above: isNat U31 tt
 isNat(x1)	status: []	precedence above: U32 U31 tt
   U52(x1,x2,x3)	status: [x2,x3,x1]	precedence above: s #mark U32 isNat plus U31 tt U51 U41
  plus(x1,x2)	status: [x2,x1]	precedence above: s #mark U32 isNat U52 U31 tt U51 U41
   U61(x1)	status: []	precedence above: 0
 #U51(x1,x2,x3)	status: [x1]	precedence above:
 #U11(x1,x2)	status: [x1,x2]	precedence above:
active(x1)	status: x1
   U31(x1,x2)	status: []	precedence above: U32 isNat tt
 #U41(x1,x2)	status: [x2,x1]	precedence above:
#active(x1)	status: x1
 #U21(x1)	status: []	precedence above:
    tt()	status: []	precedence above: U32 isNat U31
 #U71(x1,x2,x3)	status: [x2,x1,x3]	precedence above:
   U51(x1,x2,x3)	status: [x2,x3,x1]	precedence above: s #mark U32 isNat U52 plus U31 tt U41
   U41(x1,x2)	status: x2
 #U31(x1,x2)	status: [x1,x2]	precedence above:
 #U61(x1)	status: []	precedence above:
    Usable rules: { 1..92 }
    Removed DPs: #38 #55 #67 #106 #112 #126 #135
Number of SCCs: 10, DPs: 7, edges: 17
	SCC { #27 #34 #45 #47 #61 #75 #102 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
 #U72(x1,x2,x3)	status: [x3,x2,x1]	precedence above:
 #U32(x1)	status: []	precedence above:
   U21(x1)	status: x1
   U11(x1,x2)	status: x1
     s(x1)	status: [x1]	precedence above: #mark U32 isNat U31 #active tt U41
#isNat(x1)	status: []	precedence above:
   U71(x1,x2,x3)	status: [x2,x3,x1]	precedence above: U21 s U72 x #mark mark U32 isNat U52 plus U31 #active tt U51 U41
#plus(x1,x2)	status: [x2,x1]	precedence above:
   U72(x1,x2,x3)	status: [x2,x3,x1]	precedence above: U21 s U71 x #mark mark U32 isNat U52 plus U31 #active tt U51 U41
 #U52(x1,x2,x3)	status: [x3]	precedence above:
   U12(x1)	status: x1
     x(x1,x2)	status: [x2,x1]	precedence above: U21 s U71 U72 #mark mark U32 isNat U52 plus U31 #active tt U51 U41
 #U12(x1)	status: []	precedence above:
#mark(x1)	status: [x1]	precedence above: U32 isNat U31 #active tt U41
     0()	status: []	precedence above: U61
   #x(x1,x2)	status: [x1,x2]	precedence above:
   #s(x1)	status: []	precedence above:
  mark(x1)	status: x1
   U32(x1)	status: []	precedence above: isNat U31 tt
 isNat(x1)	status: []	precedence above: U32 U31 tt
   U52(x1,x2,x3)	status: [x2,x3,x1]	precedence above: s #mark U32 isNat plus U31 #active tt U51 U41
  plus(x1,x2)	status: [x2,x1]	precedence above: s #mark U32 isNat U52 U31 #active tt U51 U41
   U61(x1)	status: []	precedence above: 0
 #U51(x1,x2,x3)	status: [x1]	precedence above:
 #U11(x1,x2)	status: [x1,x2]	precedence above:
active(x1)	status: x1
   U31(x1,x2)	status: []	precedence above: U32 isNat tt
 #U41(x1,x2)	status: [x2,x1]	precedence above:
#active(x1)	status: [x1]	precedence above: #mark U32 isNat U31 tt U41
 #U21(x1)	status: []	precedence above:
    tt()	status: []	precedence above: U32 isNat U31
 #U71(x1,x2,x3)	status: [x2,x1,x3]	precedence above:
   U51(x1,x2,x3)	status: [x2,x3,x1]	precedence above: s #mark U32 isNat U52 plus U31 #active tt U41
   U41(x1,x2)	status: [x2]	precedence above: #mark U32 isNat U31 #active tt
 #U31(x1,x2)	status: [x1,x2]	precedence above:
 #U61(x1)	status: []	precedence above:
    Usable rules: { 1..92 }
    Removed DPs: #27
Number of SCCs: 10, DPs: 5, edges: 10
	SCC { #34 #45 #47 #61 #75 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
 #U72(x1,x2,x3)	weight: 0
 #U32(x1)	weight: 0
   U21(x1)	weight: max{0, (/ 1 4) + x1}
   U11(x1,x2)	weight: max{0, (/ 1 8) + x1, (/ 1 2) + x2}
     s(x1)	weight: max{0, (/ 3 8) + x1}
#isNat(x1)	weight: 0
   U71(x1,x2,x3)	weight: 0
#plus(x1,x2)	weight: 0
   U72(x1,x2,x3)	weight: 0
 #U52(x1,x2,x3)	weight: 0
   U12(x1)	weight: 0
     x(x1,x2)	weight: 0
 #U12(x1)	weight: 0
#mark(x1)	weight: max{0, (- (/ 1 16)) + x1}
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: max{0, x1}
   U32(x1)	weight: 0
 isNat(x1)	weight: max{0, (/ 1 4) + x1}
   U52(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: max{0, (/ 1 4) + x1, (/ 3 8) + x2}
   U61(x1)	weight: 0
 #U51(x1,x2,x3)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: max{0, x1}
   U31(x1,x2)	weight: 0
 #U41(x1,x2)	weight: 0
#active(x1)	weight: max{0, (- (/ 1 8)) + x1}
 #U21(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2,x3)	weight: 0
   U51(x1,x2,x3)	weight: 0
   U41(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
 #U61(x1)	weight: 0
    Usable rules: { 37..40 43 44 }
    Removed DPs: #34 #45 #47 #61 #75
Number of SCCs: 9, DPs: 0, edges: 0
YES