Input TRS:
    1: active(|2nd|(cons1(X,cons(Y,Z)))) -> mark(Y)
    2: active(|2nd|(cons(X,X1))) -> mark(|2nd|(cons1(X,X1)))
    3: active(from(X)) -> mark(cons(X,from(s(X))))
    4: mark(|2nd|(X)) -> active(|2nd|(mark(X)))
    5: mark(cons1(X1,X2)) -> active(cons1(mark(X1),mark(X2)))
    6: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
    7: mark(from(X)) -> active(from(mark(X)))
    8: mark(s(X)) -> active(s(mark(X)))
    9: |2nd|(mark(X)) -> |2nd|(X)
    10: |2nd|(active(X)) -> |2nd|(X)
    11: cons1(mark(X1),X2) -> cons1(X1,X2)
    12: cons1(X1,mark(X2)) -> cons1(X1,X2)
    13: cons1(active(X1),X2) -> cons1(X1,X2)
    14: cons1(X1,active(X2)) -> cons1(X1,X2)
    15: cons(mark(X1),X2) -> cons(X1,X2)
    16: cons(X1,mark(X2)) -> cons(X1,X2)
    17: cons(active(X1),X2) -> cons(X1,X2)
    18: cons(X1,active(X2)) -> cons(X1,X2)
    19: from(mark(X)) -> from(X)
    20: from(active(X)) -> from(X)
    21: s(mark(X)) -> s(X)
    22: s(active(X)) -> s(X)
Number of strict rules: 22
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(|2nd|(cons(X,X1))) -> #mark(|2nd|(cons1(X,X1)))
   #2: #active(|2nd|(cons(X,X1))) -> #|2nd|(cons1(X,X1))
   #3: #active(|2nd|(cons(X,X1))) -> #cons1(X,X1)
   #4: #mark(cons(X1,X2)) -> #active(cons(mark(X1),X2))
   #5: #mark(cons(X1,X2)) -> #cons(mark(X1),X2)
   #6: #mark(cons(X1,X2)) -> #mark(X1)
   #7: #cons1(active(X1),X2) -> #cons1(X1,X2)
   #8: #|2nd|(mark(X)) -> #|2nd|(X)
   #9: #cons1(mark(X1),X2) -> #cons1(X1,X2)
   #10: #cons1(X1,mark(X2)) -> #cons1(X1,X2)
   #11: #cons1(X1,active(X2)) -> #cons1(X1,X2)
   #12: #from(active(X)) -> #from(X)
   #13: #mark(from(X)) -> #active(from(mark(X)))
   #14: #mark(from(X)) -> #from(mark(X))
   #15: #mark(from(X)) -> #mark(X)
   #16: #|2nd|(active(X)) -> #|2nd|(X)
   #17: #mark(cons1(X1,X2)) -> #active(cons1(mark(X1),mark(X2)))
   #18: #mark(cons1(X1,X2)) -> #cons1(mark(X1),mark(X2))
   #19: #mark(cons1(X1,X2)) -> #mark(X1)
   #20: #mark(cons1(X1,X2)) -> #mark(X2)
   #21: #s(active(X)) -> #s(X)
   #22: #cons(active(X1),X2) -> #cons(X1,X2)
   #23: #from(mark(X)) -> #from(X)
   #24: #s(mark(X)) -> #s(X)
   #25: #cons(X1,mark(X2)) -> #cons(X1,X2)
   #26: #active(from(X)) -> #mark(cons(X,from(s(X))))
   #27: #active(from(X)) -> #cons(X,from(s(X)))
   #28: #active(from(X)) -> #from(s(X))
   #29: #active(from(X)) -> #s(X)
   #30: #active(|2nd|(cons1(X,cons(Y,Z)))) -> #mark(Y)
   #31: #mark(s(X)) -> #active(s(mark(X)))
   #32: #mark(s(X)) -> #s(mark(X))
   #33: #mark(s(X)) -> #mark(X)
   #34: #cons(mark(X1),X2) -> #cons(X1,X2)
   #35: #mark(|2nd|(X)) -> #active(|2nd|(mark(X)))
   #36: #mark(|2nd|(X)) -> #|2nd|(mark(X))
   #37: #mark(|2nd|(X)) -> #mark(X)
   #38: #cons(X1,active(X2)) -> #cons(X1,X2)
Number of SCCs: 6, DPs: 25, edges: 106
	SCC { #8 #16 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#cons1(x1,x2)	weight: 0
 |2nd|(x1)	weight: 0
#|2nd|(x1)	weight: x1
 cons1(x1,x2)	weight: 0
#mark(x1)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #8 #16
Number of SCCs: 5, DPs: 23, edges: 102
	SCC { #21 #24 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#cons1(x1,x2)	weight: 0
 |2nd|(x1)	weight: 0
#|2nd|(x1)	weight: 0
 cons1(x1,x2)	weight: 0
#mark(x1)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: x1
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #21 #24
Number of SCCs: 4, DPs: 21, edges: 98
	SCC { #12 #23 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#cons1(x1,x2)	weight: 0
 |2nd|(x1)	weight: 0
#|2nd|(x1)	weight: 0
 cons1(x1,x2)	weight: 0
#mark(x1)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: x1
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #12 #23
Number of SCCs: 3, DPs: 19, edges: 94
	SCC { #7 #9..11 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#cons1(x1,x2)	weight: x2
 |2nd|(x1)	weight: 0
#|2nd|(x1)	weight: 0
 cons1(x1,x2)	weight: 0
#mark(x1)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #10 #11
Number of SCCs: 3, DPs: 17, edges: 82
	SCC { #7 #9 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#cons1(x1,x2)	weight: x1
 |2nd|(x1)	weight: 0
#|2nd|(x1)	weight: 0
 cons1(x1,x2)	weight: 0
#mark(x1)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #7 #9
Number of SCCs: 2, DPs: 15, edges: 78
	SCC { #22 #25 #34 #38 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: x2
     s(x1)	weight: 0
#cons1(x1,x2)	weight: 0
 |2nd|(x1)	weight: 0
#|2nd|(x1)	weight: 0
 cons1(x1,x2)	weight: 0
#mark(x1)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #25 #38
Number of SCCs: 3, DPs: 13, edges: 66
	SCC { #22 #34 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: x1
     s(x1)	weight: 0
#cons1(x1,x2)	weight: 0
 |2nd|(x1)	weight: 0
#|2nd|(x1)	weight: 0
 cons1(x1,x2)	weight: 0
#mark(x1)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #22 #34
Number of SCCs: 2, DPs: 11, edges: 62
	SCC { #1 #6 #13 #15 #19 #20 #26 #30 #33 #35 #37 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#cons1(x1,x2)	weight: 0
 |2nd|(x1)	weight: (/ 1 2) + x1
#|2nd|(x1)	weight: 0
 cons1(x1,x2)	weight: max{x2, x1}
#mark(x1)	weight: x1
  from(x1)	weight: (/ 1 2) + x1
   #s(x1)	weight: 0
  mark(x1)	weight: x1
#from(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: max{x2, x1}
#active(x1)	weight: x1
    Usable rules: { 1..22 }
    Removed DPs: #15 #30 #37
Number of SCCs: 4, DPs: 8, edges: 24
	SCC { #1 #35 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (max (/ 3 32) 0)
#cons1(x1,x2)	weight: 0
 |2nd|(x1)	weight: max{0, (/ 3 32) + x1}
#|2nd|(x1)	weight: 0
 cons1(x1,x2)	weight: max{0, (- (/ 1 8)) + x1, (- (/ 11 32)) + x2}
#mark(x1)	weight: max{0, (/ 9 32) + x1}
  from(x1)	weight: max{0, (/ 3 8) + x1}
   #s(x1)	weight: 0
  mark(x1)	weight: max{0, (/ 1 16) + x1}
#from(x1)	weight: 0
active(x1)	weight: max{0, x1}
  cons(x1,x2)	weight: max{0, (/ 5 16) + x1, (- (/ 5 32)) + x2}
#active(x1)	weight: max{0, (/ 3 32) + x1}
    Usable rules: { 1..22 }
    Removed DPs: #35
Number of SCCs: 3, DPs: 6, edges: 22
	SCC { #6 #13 #19 #20 #26 #33 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#cons1(x1,x2)	weight: 0
 |2nd|(x1)	weight: (/ 1 4) + x1
#|2nd|(x1)	weight: 0
 cons1(x1,x2)	weight: max{x2, (/ 1 4) + x1}
#mark(x1)	weight: x1
  from(x1)	weight: (/ 1 2) + x1
   #s(x1)	weight: 0
  mark(x1)	weight: x1
#from(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: max{x2, (/ 1 4) + x1}
#active(x1)	weight: x1
    Usable rules: { 1..22 }
    Removed DPs: #6 #19
Number of SCCs: 3, DPs: 2, edges: 4
	SCC { #20 #33 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
#cons1(x1,x2)	weight: 0
 |2nd|(x1)	weight: (/ 1 2)
#|2nd|(x1)	weight: 0
 cons1(x1,x2)	weight: (/ 1 4) + x2
#mark(x1)	weight: x1
  from(x1)	weight: (/ 1 4)
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2)
  cons(x1,x2)	weight: (/ 1 4)
#active(x1)	weight: (/ 1 4)
    Usable rules: { }
    Removed DPs: #20 #33
Number of SCCs: 2, DPs: 0, edges: 0
YES