Input TRS:
    1: active(first(0(),X)) -> mark(nil())
    2: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
    3: active(from(X)) -> mark(cons(X,from(s(X))))
    4: active(first(X1,X2)) -> first(active(X1),X2)
    5: active(first(X1,X2)) -> first(X1,active(X2))
    6: active(s(X)) -> s(active(X))
    7: active(cons(X1,X2)) -> cons(active(X1),X2)
    8: active(from(X)) -> from(active(X))
    9: first(mark(X1),X2) -> mark(first(X1,X2))
    10: first(X1,mark(X2)) -> mark(first(X1,X2))
    11: s(mark(X)) -> mark(s(X))
    12: cons(mark(X1),X2) -> mark(cons(X1,X2))
    13: from(mark(X)) -> mark(from(X))
    14: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
    15: proper(0()) -> ok(0())
    16: proper(nil()) -> ok(nil())
    17: proper(s(X)) -> s(proper(X))
    18: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    19: proper(from(X)) -> from(proper(X))
    20: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
    21: s(ok(X)) -> ok(s(X))
    22: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    23: from(ok(X)) -> ok(from(X))
    24: top(mark(X)) -> top(proper(X))
    25: top(ok(X)) -> top(active(X))
Number of strict rules: 25
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(first(s(X),cons(Y,Z))) -> #cons(Y,first(X,Z))
   #2: #active(first(s(X),cons(Y,Z))) -> #first(X,Z)
   #3: #active(s(X)) -> #s(active(X))
   #4: #active(s(X)) -> #active(X)
   #5: #from(mark(X)) -> #from(X)
   #6: #first(mark(X1),X2) -> #first(X1,X2)
   #7: #s(mark(X)) -> #s(X)
   #8: #top(mark(X)) -> #top(proper(X))
   #9: #top(mark(X)) -> #proper(X)
   #10: #from(ok(X)) -> #from(X)
   #11: #cons(mark(X1),X2) -> #cons(X1,X2)
   #12: #proper(first(X1,X2)) -> #first(proper(X1),proper(X2))
   #13: #proper(first(X1,X2)) -> #proper(X1)
   #14: #proper(first(X1,X2)) -> #proper(X2)
   #15: #top(ok(X)) -> #top(active(X))
   #16: #top(ok(X)) -> #active(X)
   #17: #first(ok(X1),ok(X2)) -> #first(X1,X2)
   #18: #active(cons(X1,X2)) -> #cons(active(X1),X2)
   #19: #active(cons(X1,X2)) -> #active(X1)
   #20: #first(X1,mark(X2)) -> #first(X1,X2)
   #21: #active(first(X1,X2)) -> #first(X1,active(X2))
   #22: #active(first(X1,X2)) -> #active(X2)
   #23: #cons(ok(X1),ok(X2)) -> #cons(X1,X2)
   #24: #proper(s(X)) -> #s(proper(X))
   #25: #proper(s(X)) -> #proper(X)
   #26: #proper(from(X)) -> #from(proper(X))
   #27: #proper(from(X)) -> #proper(X)
   #28: #s(ok(X)) -> #s(X)
   #29: #active(from(X)) -> #cons(X,from(s(X)))
   #30: #active(from(X)) -> #from(s(X))
   #31: #active(from(X)) -> #s(X)
   #32: #active(from(X)) -> #from(active(X))
   #33: #active(from(X)) -> #active(X)
   #34: #active(first(X1,X2)) -> #first(active(X1),X2)
   #35: #active(first(X1,X2)) -> #active(X1)
   #36: #proper(cons(X1,X2)) -> #cons(proper(X1),proper(X2))
   #37: #proper(cons(X1,X2)) -> #proper(X1)
   #38: #proper(cons(X1,X2)) -> #proper(X2)
Number of SCCs: 7, DPs: 22, edges: 86
	SCC { #5 #10 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
   top(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 first(x1,x2)	weight: 0
#proper(x1)	weight: 0
#from(x1)	weight: x1
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #5 #10
Number of SCCs: 6, DPs: 20, edges: 82
	SCC { #7 #28 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
   top(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: x1
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 first(x1,x2)	weight: 0
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #7 #28
Number of SCCs: 5, DPs: 18, edges: 78
	SCC { #8 #15 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
 #top(x1)	weight: x1
proper(x1)	weight: x1
    ok(x1)	weight: x1
     0()	weight: 0
  from(x1)	weight: (/ 1 2) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
 first(x1,x2)	weight: (/ 1 4) + x1 + x2
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x1
#active(x1)	weight: 0
    Usable rules: { 1..23 }
    Removed DPs: #8
Number of SCCs: 5, DPs: 17, edges: 75
	SCC { #15 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
 #top(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
  from(x1)	weight: (/ 1 2) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: x1
 first(x1,x2)	weight: (/ 1 4) + x2
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x1
#active(x1)	weight: 0
    Usable rules: { 1..13 20..23 }
    Removed DPs: #15
Number of SCCs: 4, DPs: 16, edges: 74
	SCC { #11 #23 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: x1 + x2
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
 #top(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
  from(x1)	weight: (/ 1 2) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: x1
 first(x1,x2)	weight: (/ 1 4) + x2
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x1
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #23
Number of SCCs: 5, DPs: 15, edges: 71
	SCC { #11 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: x1
     s(x1)	weight: (/ 1 4)
   top(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
  from(x1)	weight: (/ 1 2)
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
 first(x1,x2)	weight: (/ 1 2)
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4)
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #11
Number of SCCs: 4, DPs: 14, edges: 70
	SCC { #6 #17 #20 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4)
   top(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
  from(x1)	weight: (/ 1 2)
   #s(x1)	weight: 0
#first(x1,x2)	weight: x1
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
 first(x1,x2)	weight: (/ 1 2)
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4)
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #6 #17
Number of SCCs: 5, DPs: 12, edges: 62
	SCC { #20 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4)
   top(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
  from(x1)	weight: (/ 1 2)
   #s(x1)	weight: 0
#first(x1,x2)	weight: x2
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
 first(x1,x2)	weight: (/ 1 2)
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4)
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #20
Number of SCCs: 4, DPs: 11, edges: 61
	SCC { #4 #19 #22 #33 #35 }
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
proper(x1)	weight: x1
    ok(x1)	weight: x1
     0()	weight: 0
  from(x1)	weight: (/ 1 2) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: x1
 first(x1,x2)	weight: (/ 1 4) + x1 + x2
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x1
#active(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #4 #19 #22 #33 #35
Number of SCCs: 4, DPs: 6, edges: 36
	SCC { #13 #14 #25 #27 #37 #38 }
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
proper(x1)	weight: x1
    ok(x1)	weight: x1
     0()	weight: 0
  from(x1)	weight: (/ 1 4) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: x1
 first(x1,x2)	weight: (/ 1 4) + x1 + x2
#proper(x1)	weight: x1
#from(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x1 + x2
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #13 #14 #25 #27 #37 #38
Number of SCCs: 3, DPs: 0, edges: 0
YES