Input TRS:
    1: active(and(tt(),X)) -> mark(X)
    2: active(plus(N,0())) -> mark(N)
    3: active(plus(N,s(M))) -> mark(s(plus(N,M)))
    4: active(x(N,0())) -> mark(0())
    5: active(x(N,s(M))) -> mark(plus(x(N,M),N))
    6: active(and(X1,X2)) -> and(active(X1),X2)
    7: active(plus(X1,X2)) -> plus(active(X1),X2)
    8: active(plus(X1,X2)) -> plus(X1,active(X2))
    9: active(s(X)) -> s(active(X))
    10: active(x(X1,X2)) -> x(active(X1),X2)
    11: active(x(X1,X2)) -> x(X1,active(X2))
    12: and(mark(X1),X2) -> mark(and(X1,X2))
    13: plus(mark(X1),X2) -> mark(plus(X1,X2))
    14: plus(X1,mark(X2)) -> mark(plus(X1,X2))
    15: s(mark(X)) -> mark(s(X))
    16: x(mark(X1),X2) -> mark(x(X1,X2))
    17: x(X1,mark(X2)) -> mark(x(X1,X2))
    18: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
    19: proper(tt()) -> ok(tt())
    20: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
    21: proper(0()) -> ok(0())
    22: proper(s(X)) -> s(proper(X))
    23: proper(x(X1,X2)) -> x(proper(X1),proper(X2))
    24: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
    25: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
    26: s(ok(X)) -> ok(s(X))
    27: x(ok(X1),ok(X2)) -> ok(x(X1,X2))
    28: top(mark(X)) -> top(proper(X))
    29: top(ok(X)) -> top(active(X))
Number of strict rules: 29
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #top(ok(X)) -> #top(active(X))
   #2: #top(ok(X)) -> #active(X)
   #3: #active(and(X1,X2)) -> #and(active(X1),X2)
   #4: #active(and(X1,X2)) -> #active(X1)
   #5: #plus(mark(X1),X2) -> #plus(X1,X2)
   #6: #active(s(X)) -> #s(active(X))
   #7: #active(s(X)) -> #active(X)
   #8: #active(x(X1,X2)) -> #x(X1,active(X2))
   #9: #active(x(X1,X2)) -> #active(X2)
   #10: #and(ok(X1),ok(X2)) -> #and(X1,X2)
   #11: #proper(x(X1,X2)) -> #x(proper(X1),proper(X2))
   #12: #proper(x(X1,X2)) -> #proper(X1)
   #13: #proper(x(X1,X2)) -> #proper(X2)
   #14: #and(mark(X1),X2) -> #and(X1,X2)
   #15: #plus(X1,mark(X2)) -> #plus(X1,X2)
   #16: #plus(ok(X1),ok(X2)) -> #plus(X1,X2)
   #17: #proper(plus(X1,X2)) -> #plus(proper(X1),proper(X2))
   #18: #proper(plus(X1,X2)) -> #proper(X1)
   #19: #proper(plus(X1,X2)) -> #proper(X2)
   #20: #active(plus(X1,X2)) -> #plus(active(X1),X2)
   #21: #active(plus(X1,X2)) -> #active(X1)
   #22: #active(x(X1,X2)) -> #x(active(X1),X2)
   #23: #active(x(X1,X2)) -> #active(X1)
   #24: #active(x(N,s(M))) -> #plus(x(N,M),N)
   #25: #active(x(N,s(M))) -> #x(N,M)
   #26: #top(mark(X)) -> #top(proper(X))
   #27: #top(mark(X)) -> #proper(X)
   #28: #proper(s(X)) -> #s(proper(X))
   #29: #proper(s(X)) -> #proper(X)
   #30: #x(ok(X1),ok(X2)) -> #x(X1,X2)
   #31: #x(X1,mark(X2)) -> #x(X1,X2)
   #32: #s(ok(X)) -> #s(X)
   #33: #x(mark(X1),X2) -> #x(X1,X2)
   #34: #active(plus(N,s(M))) -> #s(plus(N,M))
   #35: #active(plus(N,s(M))) -> #plus(N,M)
   #36: #active(plus(X1,X2)) -> #plus(X1,active(X2))
   #37: #active(plus(X1,X2)) -> #active(X2)
   #38: #s(mark(X)) -> #s(X)
   #39: #proper(and(X1,X2)) -> #and(proper(X1),proper(X2))
   #40: #proper(and(X1,X2)) -> #proper(X1)
   #41: #proper(and(X1,X2)) -> #proper(X2)
Number of SCCs: 7, DPs: 25, edges: 115
	SCC { #32 #38 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
     x(x1,x2)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: x1
  mark(x1)	weight: (/ 1 2) + x1
#proper(x1)	weight: 0
  plus(x1,x2)	weight: 0
active(x1)	weight: 0
#active(x1)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #32 #38
Number of SCCs: 6, DPs: 23, edges: 111
	SCC { #1 #26 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
     s(x1)	status: [x1]	precedence above: mark
   top(x1)	status: []	precedence above:
   and(x1,x2)	status: [x1,x2]	precedence above: proper mark
#plus(x1,x2)	status: [x2]	precedence above:
 #top(x1)	status: [x1]	precedence above:
     x(x1,x2)	status: [x1,x2]	precedence above: s ok 0 mark plus
proper(x1)	status: x1
    ok(x1)	status: x1
     0()	status: []	precedence above: s ok mark plus
   #x(x1,x2)	status: [x2]	precedence above:
   #s(x1)	status: []	precedence above:
  mark(x1)	status: [x1]	precedence above:
#proper(x1)	status: []	precedence above:
  plus(x1,x2)	status: [x1,x2]	precedence above: s ok mark
active(x1)	status: x1
#active(x1)	status: []	precedence above:
    tt()	status: []	precedence above:
 #and(x1,x2)	status: [x2]	precedence above:
    Usable rules: { 1..27 }
    Removed DPs: #26
Number of SCCs: 6, DPs: 22, edges: 108
	SCC { #1 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: x1
     x(x1,x2)	weight: (/ 1 4) + x2
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4)
#proper(x1)	weight: 0
  plus(x1,x2)	weight: (/ 1 4) + x2
active(x1)	weight: (/ 1 4) + x1
#active(x1)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { 1..17 24..27 }
    Removed DPs: #1
Number of SCCs: 5, DPs: 21, edges: 107
	SCC { #10 #14 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: x1
     x(x1,x2)	weight: (/ 1 4) + x2
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4)
#proper(x1)	weight: 0
  plus(x1,x2)	weight: (/ 1 4) + x2
active(x1)	weight: (/ 1 4) + x1
#active(x1)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: x2
    Usable rules: { }
    Removed DPs: #10
Number of SCCs: 6, DPs: 20, edges: 104
	SCC { #14 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 4) + x2
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
  plus(x1,x2)	weight: (/ 1 4) + x2
active(x1)	weight: (/ 1 4) + x1
#active(x1)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: x1
    Usable rules: { }
    Removed DPs: #14
Number of SCCs: 5, DPs: 19, edges: 103
	SCC { #5 #15 #16 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x2
#plus(x1,x2)	weight: x2
 #top(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 4) + x2
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
  plus(x1,x2)	weight: (/ 1 4) + x2
active(x1)	weight: (/ 1 4) + x1
#active(x1)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #15 #16
Number of SCCs: 6, DPs: 17, edges: 95
	SCC { #5 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x2
#plus(x1,x2)	weight: x1
 #top(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 4) + x2
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
  plus(x1,x2)	weight: (/ 1 4) + x2
active(x1)	weight: (/ 1 4) + x1
#active(x1)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #5
Number of SCCs: 5, DPs: 16, edges: 94
	SCC { #30 #31 #33 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 4) + x2
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #x(x1,x2)	weight: x1 + x2
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
  plus(x1,x2)	weight: (/ 1 4) + x2
active(x1)	weight: (/ 1 4) + x1
#active(x1)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #30 #31 #33
Number of SCCs: 5, DPs: 13, edges: 85
	SCC { #4 #7 #9 #21 #23 #37 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x1 + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 4) + x1 + x2
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
  plus(x1,x2)	weight: (/ 1 4) + x1 + x2
active(x1)	weight: (/ 1 4) + x1
#active(x1)	weight: x1
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #4 #7 #9 #21 #23 #37
Number of SCCs: 4, DPs: 7, edges: 49
	SCC { #12 #13 #18 #19 #29 #40 #41 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x1 + x2
#plus(x1,x2)	weight: 0
 #top(x1)	weight: 0
     x(x1,x2)	weight: (/ 1 4) + x1 + x2
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #x(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: x1
  plus(x1,x2)	weight: (/ 1 4) + x1 + x2
active(x1)	weight: (/ 1 4) + x1
#active(x1)	weight: 0
    tt()	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #12 #13 #18 #19 #29 #40 #41
Number of SCCs: 3, DPs: 0, edges: 0
YES