Input TRS:
    1: active(f(X)) -> mark(cons(X,f(g(X))))
    2: active(g(0())) -> mark(s(0()))
    3: active(g(s(X))) -> mark(s(s(g(X))))
    4: active(sel(0(),cons(X,Y))) -> mark(X)
    5: active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
    6: active(f(X)) -> f(active(X))
    7: active(cons(X1,X2)) -> cons(active(X1),X2)
    8: active(g(X)) -> g(active(X))
    9: active(s(X)) -> s(active(X))
    10: active(sel(X1,X2)) -> sel(active(X1),X2)
    11: active(sel(X1,X2)) -> sel(X1,active(X2))
    12: f(mark(X)) -> mark(f(X))
    13: cons(mark(X1),X2) -> mark(cons(X1,X2))
    14: g(mark(X)) -> mark(g(X))
    15: s(mark(X)) -> mark(s(X))
    16: sel(mark(X1),X2) -> mark(sel(X1,X2))
    17: sel(X1,mark(X2)) -> mark(sel(X1,X2))
    18: proper(f(X)) -> f(proper(X))
    19: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    20: proper(g(X)) -> g(proper(X))
    21: proper(0()) -> ok(0())
    22: proper(s(X)) -> s(proper(X))
    23: proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
    24: f(ok(X)) -> ok(f(X))
    25: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    26: g(ok(X)) -> ok(g(X))
    27: s(ok(X)) -> ok(s(X))
    28: sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
    29: top(mark(X)) -> top(proper(X))
    30: top(ok(X)) -> top(active(X))
Number of strict rules: 30
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(g(0())) -> #s(0())
   #2: #top(mark(X)) -> #top(proper(X))
   #3: #top(mark(X)) -> #proper(X)
   #4: #active(f(X)) -> #f(active(X))
   #5: #active(f(X)) -> #active(X)
   #6: #cons(mark(X1),X2) -> #cons(X1,X2)
   #7: #active(s(X)) -> #s(active(X))
   #8: #active(s(X)) -> #active(X)
   #9: #active(sel(X1,X2)) -> #sel(X1,active(X2))
   #10: #active(sel(X1,X2)) -> #active(X2)
   #11: #f(ok(X)) -> #f(X)
   #12: #proper(sel(X1,X2)) -> #sel(proper(X1),proper(X2))
   #13: #proper(sel(X1,X2)) -> #proper(X1)
   #14: #proper(sel(X1,X2)) -> #proper(X2)
   #15: #f(mark(X)) -> #f(X)
   #16: #g(mark(X)) -> #g(X)
   #17: #top(ok(X)) -> #top(active(X))
   #18: #top(ok(X)) -> #active(X)
   #19: #cons(ok(X1),ok(X2)) -> #cons(X1,X2)
   #20: #proper(g(X)) -> #g(proper(X))
   #21: #proper(g(X)) -> #proper(X)
   #22: #active(cons(X1,X2)) -> #cons(active(X1),X2)
   #23: #active(cons(X1,X2)) -> #active(X1)
   #24: #active(sel(X1,X2)) -> #sel(active(X1),X2)
   #25: #active(sel(X1,X2)) -> #active(X1)
   #26: #active(sel(s(X),cons(Y,Z))) -> #sel(X,Z)
   #27: #sel(ok(X1),ok(X2)) -> #sel(X1,X2)
   #28: #proper(s(X)) -> #s(proper(X))
   #29: #proper(s(X)) -> #proper(X)
   #30: #s(ok(X)) -> #s(X)
   #31: #sel(X1,mark(X2)) -> #sel(X1,X2)
   #32: #proper(cons(X1,X2)) -> #cons(proper(X1),proper(X2))
   #33: #proper(cons(X1,X2)) -> #proper(X1)
   #34: #proper(cons(X1,X2)) -> #proper(X2)
   #35: #g(ok(X)) -> #g(X)
   #36: #sel(mark(X1),X2) -> #sel(X1,X2)
   #37: #active(g(s(X))) -> #s(s(g(X)))
   #38: #active(g(s(X))) -> #s(g(X))
   #39: #active(g(s(X))) -> #g(X)
   #40: #active(f(X)) -> #cons(X,f(g(X)))
   #41: #active(f(X)) -> #f(g(X))
   #42: #active(f(X)) -> #g(X)
   #43: #active(g(X)) -> #g(active(X))
   #44: #active(g(X)) -> #active(X)
   #45: #s(mark(X)) -> #s(X)
   #46: #proper(f(X)) -> #f(proper(X))
   #47: #proper(f(X)) -> #proper(X)
Number of SCCs: 8, DPs: 26, edges: 114
	SCC { #16 #35 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
   top(x1)	weight: 0
 #top(x1)	weight: 0
     f(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   #f(x1)	weight: 0
   #g(x1)	weight: x1
#proper(x1)	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
     g(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #16 #35
Number of SCCs: 7, DPs: 24, edges: 110
	SCC { #11 #15 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
   top(x1)	weight: 0
 #top(x1)	weight: 0
     f(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   #f(x1)	weight: x1
   #g(x1)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
     g(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #11 #15
Number of SCCs: 6, DPs: 22, edges: 106
	SCC { #30 #45 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
   top(x1)	weight: 0
 #top(x1)	weight: 0
     f(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
   #s(x1)	weight: x1
  mark(x1)	weight: (/ 1 2) + x1
   #f(x1)	weight: 0
   #g(x1)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
     g(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #30 #45
Number of SCCs: 5, DPs: 20, edges: 102
	SCC { #2 #17 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded.
#cons(x1,x2)	weight: (/ 1 8) + x2 + x1	status: [x1,x2]	precedence above:
     s(x1)	weight: x1	status: [x1]	precedence above: ok mark active
   top(x1)	weight: x1	status: []	precedence above:
 #top(x1)	weight: x1	status: [x1]	precedence above:
     f(x1)	weight: (/ 1 4) + x1	status: [x1]	precedence above: s proper ok 0 sel mark active cons g
proper(x1)	weight: x1	status: x1
    ok(x1)	weight: x1	status: x1
     0()	weight: (/ 1 8)	status: []	precedence above:
 #sel(x1,x2)	weight: x2	status: []	precedence above:
   sel(x1,x2)	weight: (/ 1 4) + x2 + x1	status: [x1,x2]	precedence above: mark
   #s(x1)	weight: (/ 1 8)	status: []	precedence above:
  mark(x1)	weight: x1	status: [x1]	precedence above:
   #f(x1)	weight: (/ 1 8)	status: []	precedence above:
   #g(x1)	weight: x1	status: []	precedence above:
#proper(x1)	weight: (/ 1 8)	status: []	precedence above:
active(x1)	weight: x1	status: x1
  cons(x1,x2)	weight: max{x2, (/ 1 8) + x1}	status: [x1]	precedence above: proper sel mark
#active(x1)	weight: x1	status: []	precedence above:
     g(x1)	weight: x1	status: [x1]	precedence above: s ok 0 sel mark active
    Usable rules: { 1..28 }
    Removed DPs: #2
Number of SCCs: 5, DPs: 19, edges: 99
	SCC { #17 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
   top(x1)	weight: 0
 #top(x1)	weight: x1
     f(x1)	weight: x1
proper(x1)	weight: (/ 1 2)
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x1
   #s(x1)	weight: 0
  mark(x1)	weight: 0
   #f(x1)	weight: 0
   #g(x1)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: x1
#active(x1)	weight: 0
     g(x1)	weight: x1
    Usable rules: { 1..17 24..28 }
    Removed DPs: #17
Number of SCCs: 4, DPs: 18, edges: 98
	SCC { #6 #19 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: x2
     s(x1)	weight: x1
   top(x1)	weight: 0
 #top(x1)	weight: x1
     f(x1)	weight: x1
proper(x1)	weight: (/ 1 2)
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x1
   #s(x1)	weight: 0
  mark(x1)	weight: 0
   #f(x1)	weight: 0
   #g(x1)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: x1
#active(x1)	weight: 0
     g(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #19
Number of SCCs: 5, DPs: 17, edges: 95
	SCC { #6 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: x1
     s(x1)	weight: x1
   top(x1)	weight: 0
 #top(x1)	weight: 0
     f(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x1
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   #f(x1)	weight: 0
   #g(x1)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
     g(x1)	weight: (/ 1 2)
    Usable rules: { }
    Removed DPs: #6
Number of SCCs: 4, DPs: 16, edges: 94
	SCC { #27 #31 #36 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
   top(x1)	weight: 0
 #top(x1)	weight: 0
     f(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: x1
   sel(x1,x2)	weight: x1
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   #f(x1)	weight: 0
   #g(x1)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
     g(x1)	weight: (/ 1 2)
    Usable rules: { }
    Removed DPs: #27 #36
Number of SCCs: 5, DPs: 14, edges: 86
	SCC { #31 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
   top(x1)	weight: 0
 #top(x1)	weight: 0
     f(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: x2
   sel(x1,x2)	weight: x1
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
   #f(x1)	weight: 0
   #g(x1)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
     g(x1)	weight: (/ 1 2)
    Usable rules: { }
    Removed DPs: #31
Number of SCCs: 4, DPs: 13, edges: 85
	SCC { #5 #8 #10 #23 #25 #44 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
 #top(x1)	weight: 0
     f(x1)	weight: x1
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x1 + x2
   #s(x1)	weight: 0
  mark(x1)	weight: x1
   #f(x1)	weight: 0
   #g(x1)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x1
#active(x1)	weight: x1
     g(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #8 #23
Number of SCCs: 5, DPs: 11, edges: 65
	SCC { #5 #10 #25 #44 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
 #top(x1)	weight: 0
     f(x1)	weight: (/ 1 8) + x1
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 8) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x1 + x2
   #s(x1)	weight: 0
  mark(x1)	weight: x1
   #f(x1)	weight: 0
   #g(x1)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x1
#active(x1)	weight: x1
     g(x1)	weight: (/ 1 8) + x1
    Usable rules: { }
    Removed DPs: #5 #44
Number of SCCs: 5, DPs: 9, edges: 53
	SCC { #10 #25 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
 #top(x1)	weight: 0
     f(x1)	weight: (/ 1 4) + x1
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 4) + x1 + x2
   #s(x1)	weight: 0
  mark(x1)	weight: x1
   #f(x1)	weight: 0
   #g(x1)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x1
#active(x1)	weight: x1
     g(x1)	weight: (/ 1 4) + x1
    Usable rules: { }
    Removed DPs: #10 #25
Number of SCCs: 4, DPs: 7, edges: 49
	SCC { #13 #14 #21 #29 #33 #34 #47 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
 #top(x1)	weight: 0
     f(x1)	weight: (/ 1 4) + x1
proper(x1)	weight: (/ 1 4)
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 4) + x1 + x2
   #s(x1)	weight: 0
  mark(x1)	weight: x1
   #f(x1)	weight: 0
   #g(x1)	weight: 0
#proper(x1)	weight: x1
active(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x1 + x2
#active(x1)	weight: 0
     g(x1)	weight: (/ 1 4) + x1
    Usable rules: { }
    Removed DPs: #13 #14 #21 #29 #33 #34 #47
Number of SCCs: 4, DPs: 0, edges: 0
YES