Input TRS:
    1: active(U11(tt(),N)) -> mark(N)
    2: active(U21(tt(),M,N)) -> mark(s(plus(N,M)))
    3: active(and(tt(),X)) -> mark(X)
    4: active(isNat(0())) -> mark(tt())
    5: active(isNat(plus(V1,V2))) -> mark(and(isNat(V1),isNat(V2)))
    6: active(isNat(s(V1))) -> mark(isNat(V1))
    7: active(plus(N,0())) -> mark(U11(isNat(N),N))
    8: active(plus(N,s(M))) -> mark(U21(and(isNat(M),isNat(N)),M,N))
    9: active(U11(X1,X2)) -> U11(active(X1),X2)
    10: active(U21(X1,X2,X3)) -> U21(active(X1),X2,X3)
    11: active(s(X)) -> s(active(X))
    12: active(plus(X1,X2)) -> plus(active(X1),X2)
    13: active(plus(X1,X2)) -> plus(X1,active(X2))
    14: active(and(X1,X2)) -> and(active(X1),X2)
    15: U11(mark(X1),X2) -> mark(U11(X1,X2))
    16: U21(mark(X1),X2,X3) -> mark(U21(X1,X2,X3))
    17: s(mark(X)) -> mark(s(X))
    18: plus(mark(X1),X2) -> mark(plus(X1,X2))
    19: plus(X1,mark(X2)) -> mark(plus(X1,X2))
    20: and(mark(X1),X2) -> mark(and(X1,X2))
    21: proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
    22: proper(tt()) -> ok(tt())
    23: proper(U21(X1,X2,X3)) -> U21(proper(X1),proper(X2),proper(X3))
    24: proper(s(X)) -> s(proper(X))
    25: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
    26: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
    27: proper(isNat(X)) -> isNat(proper(X))
    28: proper(0()) -> ok(0())
    29: U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
    30: U21(ok(X1),ok(X2),ok(X3)) -> ok(U21(X1,X2,X3))
    31: s(ok(X)) -> ok(s(X))
    32: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
    33: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
    34: isNat(ok(X)) -> ok(isNat(X))
    35: top(mark(X)) -> top(proper(X))
    36: top(ok(X)) -> top(active(X))
Number of strict rules: 36
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(U21(tt(),M,N)) -> #s(plus(N,M))
   #2: #active(U21(tt(),M,N)) -> #plus(N,M)
   #3: #U11(ok(X1),ok(X2)) -> #U11(X1,X2)
   #4: #top(mark(X)) -> #top(proper(X))
   #5: #top(mark(X)) -> #proper(X)
   #6: #active(isNat(s(V1))) -> #isNat(V1)
   #7: #active(plus(X1,X2)) -> #plus(X1,active(X2))
   #8: #active(plus(X1,X2)) -> #active(X2)
   #9: #active(U11(X1,X2)) -> #U11(active(X1),X2)
   #10: #active(U11(X1,X2)) -> #active(X1)
   #11: #active(s(X)) -> #s(active(X))
   #12: #active(s(X)) -> #active(X)
   #13: #proper(s(X)) -> #s(proper(X))
   #14: #proper(s(X)) -> #proper(X)
   #15: #proper(U21(X1,X2,X3)) -> #U21(proper(X1),proper(X2),proper(X3))
   #16: #proper(U21(X1,X2,X3)) -> #proper(X1)
   #17: #proper(U21(X1,X2,X3)) -> #proper(X2)
   #18: #proper(U21(X1,X2,X3)) -> #proper(X3)
   #19: #active(plus(X1,X2)) -> #plus(active(X1),X2)
   #20: #active(plus(X1,X2)) -> #active(X1)
   #21: #s(ok(X)) -> #s(X)
   #22: #active(and(X1,X2)) -> #and(active(X1),X2)
   #23: #active(and(X1,X2)) -> #active(X1)
   #24: #U21(ok(X1),ok(X2),ok(X3)) -> #U21(X1,X2,X3)
   #25: #proper(plus(X1,X2)) -> #plus(proper(X1),proper(X2))
   #26: #proper(plus(X1,X2)) -> #proper(X1)
   #27: #proper(plus(X1,X2)) -> #proper(X2)
   #28: #and(mark(X1),X2) -> #and(X1,X2)
   #29: #active(plus(N,0())) -> #U11(isNat(N),N)
   #30: #active(plus(N,0())) -> #isNat(N)
   #31: #active(U21(X1,X2,X3)) -> #U21(active(X1),X2,X3)
   #32: #active(U21(X1,X2,X3)) -> #active(X1)
   #33: #and(ok(X1),ok(X2)) -> #and(X1,X2)
   #34: #active(isNat(plus(V1,V2))) -> #and(isNat(V1),isNat(V2))
   #35: #active(isNat(plus(V1,V2))) -> #isNat(V1)
   #36: #active(isNat(plus(V1,V2))) -> #isNat(V2)
   #37: #isNat(ok(X)) -> #isNat(X)
   #38: #proper(isNat(X)) -> #isNat(proper(X))
   #39: #proper(isNat(X)) -> #proper(X)
   #40: #s(mark(X)) -> #s(X)
   #41: #plus(ok(X1),ok(X2)) -> #plus(X1,X2)
   #42: #plus(X1,mark(X2)) -> #plus(X1,X2)
   #43: #proper(and(X1,X2)) -> #and(proper(X1),proper(X2))
   #44: #proper(and(X1,X2)) -> #proper(X1)
   #45: #proper(and(X1,X2)) -> #proper(X2)
   #46: #top(ok(X)) -> #top(active(X))
   #47: #top(ok(X)) -> #active(X)
   #48: #proper(U11(X1,X2)) -> #U11(proper(X1),proper(X2))
   #49: #proper(U11(X1,X2)) -> #proper(X1)
   #50: #proper(U11(X1,X2)) -> #proper(X2)
   #51: #U21(mark(X1),X2,X3) -> #U21(X1,X2,X3)
   #52: #active(plus(N,s(M))) -> #U21(and(isNat(M),isNat(N)),M,N)
   #53: #active(plus(N,s(M))) -> #and(isNat(M),isNat(N))
   #54: #active(plus(N,s(M))) -> #isNat(M)
   #55: #active(plus(N,s(M))) -> #isNat(N)
   #56: #U11(mark(X1),X2) -> #U11(X1,X2)
   #57: #plus(mark(X1),X2) -> #plus(X1,X2)
Number of SCCs: 9, DPs: 31, edges: 187
	SCC { #37 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: x1
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: 0
#proper(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2,x3)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #37
Number of SCCs: 8, DPs: 30, edges: 186
	SCC { #21 #40 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #s(x1)	weight: x1
  mark(x1)	weight: (/ 1 2) + x1
#proper(x1)	weight: 0
 isNat(x1)	weight: 0
  plus(x1,x2)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: 0
#active(x1)	weight: 0
 #U21(x1,x2,x3)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #21 #40
Number of SCCs: 7, DPs: 28, edges: 182
	SCC { #4 #46 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
   U21(x1,x2,x3)	status: [x2,x3,x1]	precedence above: U11 s and ok mark isNat plus
   U11(x1,x2)	status: [x1,x2]	precedence above: ok mark
     s(x1)	status: [x1]	precedence above: ok mark isNat
#isNat(x1)	status: []	precedence above:
   top(x1)	status: []	precedence above:
   and(x1,x2)	status: [x2,x1]	precedence above: U11 s ok mark isNat
#plus(x1,x2)	status: [x2]	precedence above:
 #top(x1)	status: [x1]	precedence above:
proper(x1)	status: x1
    ok(x1)	status: x1
     0()	status: []	precedence above: ok mark tt
   #s(x1)	status: []	precedence above:
  mark(x1)	status: [x1]	precedence above: ok
#proper(x1)	status: []	precedence above:
 isNat(x1)	status: [x1]	precedence above: ok mark
  plus(x1,x2)	status: [x2,x1]	precedence above: U21 U11 s and ok mark isNat
 #U11(x1,x2)	status: [x2,x1]	precedence above:
active(x1)	status: x1
#active(x1)	status: []	precedence above:
 #U21(x1,x2,x3)	status: [x1,x3]	precedence above:
    tt()	status: []	precedence above:
 #and(x1,x2)	status: [x1,x2]	precedence above:
    Usable rules: { 1..34 }
    Removed DPs: #4
Number of SCCs: 7, DPs: 27, edges: 179
	SCC { #46 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: (/ 1 4) + x3
   U11(x1,x2)	weight: (/ 1 4) + x2
     s(x1)	weight: (/ 1 4) + x1
#isNat(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: x1
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 4) + x1
  plus(x1,x2)	weight: (/ 1 4) + x1
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
#active(x1)	weight: 0
 #U21(x1,x2,x3)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { 1..20 29..34 }
    Removed DPs: #46
Number of SCCs: 6, DPs: 26, edges: 178
	SCC { #28 #33 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: (/ 1 4) + x3
   U11(x1,x2)	weight: (/ 1 4) + x2
     s(x1)	weight: (/ 1 4) + x1
#isNat(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: x1
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4)
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 4) + x1
  plus(x1,x2)	weight: (/ 1 4) + x1
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
#active(x1)	weight: 0
 #U21(x1,x2,x3)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: x2
    Usable rules: { }
    Removed DPs: #33
Number of SCCs: 7, DPs: 25, edges: 175
	SCC { #28 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: (/ 1 8) + x1 + x2 + x3
   U11(x1,x2)	weight: (/ 1 8) + x1 + x2
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x1 + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: x1
proper(x1)	weight: x1
    ok(x1)	weight: x1
     0()	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 8) + x1
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8)
  plus(x1,x2)	weight: (/ 1 8) + x1 + x2
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 3 8) + x1
#active(x1)	weight: 0
 #U21(x1,x2,x3)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: x1
    Usable rules: { }
    Removed DPs: #28
Number of SCCs: 6, DPs: 24, edges: 174
	SCC { #3 #56 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: (/ 1 8) + x1 + x2 + x3
   U11(x1,x2)	weight: (/ 1 8) + x1 + x2
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x1 + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: x1
proper(x1)	weight: x1
    ok(x1)	weight: x1
     0()	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 8) + x1
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 8)
  plus(x1,x2)	weight: (/ 1 8) + x1 + x2
 #U11(x1,x2)	weight: x1
active(x1)	weight: (/ 3 8) + x1
#active(x1)	weight: 0
 #U21(x1,x2,x3)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #56
Number of SCCs: 7, DPs: 23, edges: 171
	SCC { #3 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: (/ 1 4) + x1 + x2
   U11(x1,x2)	weight: (/ 1 4)
     s(x1)	weight: (/ 1 4)
#isNat(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x1
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 4)
  plus(x1,x2)	weight: x2
 #U11(x1,x2)	weight: x1 + x2
active(x1)	weight: x1
#active(x1)	weight: 0
 #U21(x1,x2,x3)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #3
Number of SCCs: 6, DPs: 22, edges: 170
	SCC { #24 #51 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: (/ 1 4) + x1 + x2
   U11(x1,x2)	weight: (/ 1 4)
     s(x1)	weight: (/ 1 4)
#isNat(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x1
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 4)
  plus(x1,x2)	weight: x2
 #U11(x1,x2)	weight: 0
active(x1)	weight: x1
#active(x1)	weight: 0
 #U21(x1,x2,x3)	weight: x2
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #24
Number of SCCs: 7, DPs: 21, edges: 167
	SCC { #51 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: (/ 1 4) + x1 + x2
   U11(x1,x2)	weight: (/ 1 4)
     s(x1)	weight: (/ 1 4)
#isNat(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x1
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 4)
  plus(x1,x2)	weight: x2
 #U11(x1,x2)	weight: 0
active(x1)	weight: x1
#active(x1)	weight: 0
 #U21(x1,x2,x3)	weight: x1
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #51
Number of SCCs: 6, DPs: 20, edges: 166
	SCC { #41 #42 #57 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: (/ 1 4) + x1 + x2
   U11(x1,x2)	weight: (/ 1 4)
     s(x1)	weight: (/ 1 4)
#isNat(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x1
#plus(x1,x2)	weight: x1
 #top(x1)	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 4)
  plus(x1,x2)	weight: x2
 #U11(x1,x2)	weight: 0
active(x1)	weight: x1
#active(x1)	weight: 0
 #U21(x1,x2,x3)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #41 #57
Number of SCCs: 7, DPs: 18, edges: 158
	SCC { #42 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: (/ 1 4) + x1 + x2
   U11(x1,x2)	weight: (/ 1 4)
     s(x1)	weight: (/ 1 4)
#isNat(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x1
#plus(x1,x2)	weight: x2
 #top(x1)	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 4)
  plus(x1,x2)	weight: x2
 #U11(x1,x2)	weight: 0
active(x1)	weight: x1
#active(x1)	weight: 0
 #U21(x1,x2,x3)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #42
Number of SCCs: 6, DPs: 17, edges: 157
	SCC { #8 #10 #12 #20 #23 #32 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: (/ 1 4) + x1 + x2
   U11(x1,x2)	weight: (/ 1 4) + x1
     s(x1)	weight: (/ 1 4) + x1
#isNat(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x1
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#proper(x1)	weight: 0
 isNat(x1)	weight: (/ 1 4)
  plus(x1,x2)	weight: (/ 1 4) + x1 + x2
 #U11(x1,x2)	weight: 0
active(x1)	weight: x1
#active(x1)	weight: x1
 #U21(x1,x2,x3)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #8 #10 #12 #20 #23 #32
Number of SCCs: 6, DPs: 11, edges: 121
	SCC { #14 #16..18 #26 #27 #39 #44 #45 #49 #50 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   U21(x1,x2,x3)	weight: (/ 1 8) + x1 + x2 + x3
   U11(x1,x2)	weight: (/ 1 8) + x1 + x2
     s(x1)	weight: (/ 1 8) + x1
#isNat(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x1 + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 8) + x1
     0()	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: x1
 isNat(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1 + x2
 #U11(x1,x2)	weight: 0
active(x1)	weight: x1
#active(x1)	weight: 0
 #U21(x1,x2,x3)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #14 #16..18 #26 #27 #39 #44 #45 #49 #50
Number of SCCs: 5, DPs: 0, edges: 0
YES