Input TRS:
    1: active(and(true(),X)) -> mark(X)
    2: active(and(false(),Y)) -> mark(false())
    3: active(if(true(),X,Y)) -> mark(X)
    4: active(if(false(),X,Y)) -> mark(Y)
    5: active(add(0(),X)) -> mark(X)
    6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
    7: active(first(0(),X)) -> mark(nil())
    8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
    9: active(from(X)) -> mark(cons(X,from(s(X))))
    10: active(and(X1,X2)) -> and(active(X1),X2)
    11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
    12: active(add(X1,X2)) -> add(active(X1),X2)
    13: active(first(X1,X2)) -> first(active(X1),X2)
    14: active(first(X1,X2)) -> first(X1,active(X2))
    15: and(mark(X1),X2) -> mark(and(X1,X2))
    16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
    17: add(mark(X1),X2) -> mark(add(X1,X2))
    18: first(mark(X1),X2) -> mark(first(X1,X2))
    19: first(X1,mark(X2)) -> mark(first(X1,X2))
    20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
    21: proper(true()) -> ok(true())
    22: proper(false()) -> ok(false())
    23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
    24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
    25: proper(0()) -> ok(0())
    26: proper(s(X)) -> s(proper(X))
    27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
    28: proper(nil()) -> ok(nil())
    29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    30: proper(from(X)) -> from(proper(X))
    31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
    32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
    33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
    34: s(ok(X)) -> ok(s(X))
    35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
    36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    37: from(ok(X)) -> ok(from(X))
    38: top(mark(X)) -> top(proper(X))
    39: top(ok(X)) -> top(active(X))
Number of strict rules: 39
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #proper(cons(X1,X2)) -> #cons(proper(X1),proper(X2))
   #2: #proper(cons(X1,X2)) -> #proper(X1)
   #3: #proper(cons(X1,X2)) -> #proper(X2)
   #4: #first(ok(X1),ok(X2)) -> #first(X1,X2)
   #5: #from(ok(X)) -> #from(X)
   #6: #top(mark(X)) -> #top(proper(X))
   #7: #top(mark(X)) -> #proper(X)
   #8: #active(add(s(X),Y)) -> #s(add(X,Y))
   #9: #active(add(s(X),Y)) -> #add(X,Y)
   #10: #active(first(X1,X2)) -> #first(active(X1),X2)
   #11: #active(first(X1,X2)) -> #active(X1)
   #12: #active(from(X)) -> #cons(X,from(s(X)))
   #13: #active(from(X)) -> #from(s(X))
   #14: #active(from(X)) -> #s(X)
   #15: #active(if(X1,X2,X3)) -> #if(active(X1),X2,X3)
   #16: #active(if(X1,X2,X3)) -> #active(X1)
   #17: #proper(add(X1,X2)) -> #add(proper(X1),proper(X2))
   #18: #proper(add(X1,X2)) -> #proper(X1)
   #19: #proper(add(X1,X2)) -> #proper(X2)
   #20: #proper(if(X1,X2,X3)) -> #if(proper(X1),proper(X2),proper(X3))
   #21: #proper(if(X1,X2,X3)) -> #proper(X1)
   #22: #proper(if(X1,X2,X3)) -> #proper(X2)
   #23: #proper(if(X1,X2,X3)) -> #proper(X3)
   #24: #active(add(X1,X2)) -> #add(active(X1),X2)
   #25: #active(add(X1,X2)) -> #active(X1)
   #26: #and(ok(X1),ok(X2)) -> #and(X1,X2)
   #27: #active(first(X1,X2)) -> #first(X1,active(X2))
   #28: #active(first(X1,X2)) -> #active(X2)
   #29: #proper(from(X)) -> #from(proper(X))
   #30: #proper(from(X)) -> #proper(X)
   #31: #proper(and(X1,X2)) -> #and(proper(X1),proper(X2))
   #32: #proper(and(X1,X2)) -> #proper(X1)
   #33: #proper(and(X1,X2)) -> #proper(X2)
   #34: #top(ok(X)) -> #top(active(X))
   #35: #top(ok(X)) -> #active(X)
   #36: #active(and(X1,X2)) -> #and(active(X1),X2)
   #37: #active(and(X1,X2)) -> #active(X1)
   #38: #add(ok(X1),ok(X2)) -> #add(X1,X2)
   #39: #s(ok(X)) -> #s(X)
   #40: #proper(first(X1,X2)) -> #first(proper(X1),proper(X2))
   #41: #proper(first(X1,X2)) -> #proper(X1)
   #42: #proper(first(X1,X2)) -> #proper(X2)
   #43: #add(mark(X1),X2) -> #add(X1,X2)
   #44: #if(ok(X1),ok(X2),ok(X3)) -> #if(X1,X2,X3)
   #45: #first(X1,mark(X2)) -> #first(X1,X2)
   #46: #proper(s(X)) -> #s(proper(X))
   #47: #proper(s(X)) -> #proper(X)
   #48: #cons(ok(X1),ok(X2)) -> #cons(X1,X2)
   #49: #if(mark(X1),X2,X3) -> #if(X1,X2,X3)
   #50: #active(first(s(X),cons(Y,Z))) -> #cons(Y,first(X,Z))
   #51: #active(first(s(X),cons(Y,Z))) -> #first(X,Z)
   #52: #and(mark(X1),X2) -> #and(X1,X2)
   #53: #first(mark(X1),X2) -> #first(X1,X2)
Number of SCCs: 10, DPs: 32, edges: 222
	SCC { #39 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
 false()	weight: 0
 #top(x1)	weight: 0
  true()	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
    if(x1,x2,x3)	weight: 0
     0()	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: x1
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: 0
 first(x1,x2)	weight: 0
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #39
Number of SCCs: 9, DPs: 31, edges: 221
	SCC { #5 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
 false()	weight: 0
 #top(x1)	weight: 0
  true()	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
    if(x1,x2,x3)	weight: 0
     0()	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: 0
 first(x1,x2)	weight: 0
#proper(x1)	weight: 0
#from(x1)	weight: x1
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #5
Number of SCCs: 8, DPs: 30, edges: 220
	SCC { #48 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: x2
     s(x1)	weight: 0
   top(x1)	weight: 0
   and(x1,x2)	weight: 0
 false()	weight: 0
 #top(x1)	weight: 0
  true()	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
    if(x1,x2,x3)	weight: 0
     0()	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: 0
 first(x1,x2)	weight: 0
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #48
Number of SCCs: 7, DPs: 29, edges: 219
	SCC { #6 #34 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4)
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x1 + x2
 false()	weight: 0
 #top(x1)	weight: x1
  true()	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: x1
    if(x1,x2,x3)	weight: (/ 1 4) + x1 + x2 + x3
     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 4) + x1 + x2
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4)
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: (/ 1 4) + x1 + x2
 #and(x1,x2)	weight: 0
    Usable rules: { 1..37 }
    Removed DPs: #6
Number of SCCs: 7, DPs: 28, edges: 216
	SCC { #34 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x1
 false()	weight: 0
 #top(x1)	weight: x1
  true()	weight: 0
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 2) + x1
    if(x1,x2,x3)	weight: (/ 1 4) + x2
     0()	weight: 0
  from(x1)	weight: (/ 1 4) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4)
 first(x1,x2)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: (/ 1 4) + x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: (/ 1 4) + x1
 #and(x1,x2)	weight: 0
    Usable rules: { 1..19 31..37 }
    Removed DPs: #34
Number of SCCs: 6, DPs: 27, edges: 215
	SCC { #26 #52 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x1
 false()	weight: 0
 #top(x1)	weight: x1
  true()	weight: 0
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 2) + x1
    if(x1,x2,x3)	weight: (/ 1 4) + x2
     0()	weight: 0
  from(x1)	weight: (/ 1 4) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4)
 first(x1,x2)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: (/ 1 4) + x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: (/ 1 4) + x1
 #and(x1,x2)	weight: x2
    Usable rules: { }
    Removed DPs: #26
Number of SCCs: 7, DPs: 26, edges: 212
	SCC { #52 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: x1
 false()	weight: 0
 #top(x1)	weight: 0
  true()	weight: 0
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 4) + x1
    if(x1,x2,x3)	weight: (/ 1 8)
     0()	weight: 0
  from(x1)	weight: (/ 1 8) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 first(x1,x2)	weight: (/ 1 8) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 8) + x1
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: (/ 1 8) + x1
 #and(x1,x2)	weight: x1
    Usable rules: { }
    Removed DPs: #52
Number of SCCs: 6, DPs: 25, edges: 211
	SCC { #38 #43 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: x1
 false()	weight: 0
 #top(x1)	weight: 0
  true()	weight: 0
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 4) + x1
    if(x1,x2,x3)	weight: (/ 1 8)
     0()	weight: 0
  from(x1)	weight: (/ 1 8) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 first(x1,x2)	weight: (/ 1 8) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 8) + x1
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
 #add(x1,x2)	weight: x2
   add(x1,x2)	weight: (/ 1 8) + x1
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #38
Number of SCCs: 7, DPs: 24, edges: 208
	SCC { #43 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: x1
 false()	weight: 0
 #top(x1)	weight: 0
  true()	weight: 0
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 4) + x1
    if(x1,x2,x3)	weight: (/ 1 8)
     0()	weight: 0
  from(x1)	weight: (/ 1 8) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 first(x1,x2)	weight: (/ 1 8) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 8) + x1
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
 #add(x1,x2)	weight: x1
   add(x1,x2)	weight: (/ 1 8) + x1
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #43
Number of SCCs: 6, DPs: 23, edges: 207
	SCC { #44 #49 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: x1
 false()	weight: 0
 #top(x1)	weight: 0
  true()	weight: 0
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 4) + x1
    if(x1,x2,x3)	weight: (/ 1 8)
     0()	weight: 0
  from(x1)	weight: (/ 1 8) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 first(x1,x2)	weight: (/ 1 8) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 8) + x1
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: x2 + x3
#active(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: (/ 1 8) + x1
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #44
Number of SCCs: 7, DPs: 22, edges: 204
	SCC { #49 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: x1
 false()	weight: 0
 #top(x1)	weight: 0
  true()	weight: 0
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 4) + x1
    if(x1,x2,x3)	weight: (/ 1 8)
     0()	weight: 0
  from(x1)	weight: (/ 1 8) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 first(x1,x2)	weight: (/ 1 8) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 8) + x1
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: x1
#active(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: (/ 1 8) + x1
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #49
Number of SCCs: 6, DPs: 21, edges: 203
	SCC { #4 #45 #53 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: x1
 false()	weight: 0
 #top(x1)	weight: 0
  true()	weight: 0
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 4) + x1
    if(x1,x2,x3)	weight: (/ 1 8)
     0()	weight: 0
  from(x1)	weight: (/ 1 8) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: x2
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 first(x1,x2)	weight: (/ 1 8) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 8) + x1
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: (/ 1 8) + x1
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #4 #45
Number of SCCs: 7, DPs: 19, edges: 195
	SCC { #53 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: x1
 false()	weight: 0
 #top(x1)	weight: 0
  true()	weight: 0
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 4) + x1
    if(x1,x2,x3)	weight: (/ 1 8)
     0()	weight: 0
  from(x1)	weight: (/ 1 8) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: x1
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 first(x1,x2)	weight: (/ 1 8) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 8) + x1
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: (/ 1 8) + x1
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #53
Number of SCCs: 6, DPs: 18, edges: 194
	SCC { #11 #16 #25 #28 #37 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x1
 false()	weight: 0
 #top(x1)	weight: 0
  true()	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 2) + x1
    if(x1,x2,x3)	weight: (/ 1 4) + 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: (/ 3 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: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: x1
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: (/ 1 4) + x1
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #11 #16 #25 #28 #37
Number of SCCs: 6, DPs: 13, edges: 169
	SCC { #2 #3 #18 #19 #21..23 #30 #32 #33 #41 #42 #47 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 8) + x1 + x2
 false()	weight: 0
 #top(x1)	weight: 0
  true()	weight: 0
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 4) + x1
    if(x1,x2,x3)	weight: (/ 1 8) + x1 + x2 + x3
     0()	weight: 0
  from(x1)	weight: (/ 1 8) + x1
   #s(x1)	weight: 0
#first(x1,x2)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
 first(x1,x2)	weight: (/ 1 8) + x1 + x2
#proper(x1)	weight: x1
#from(x1)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 8) + x1 + x2
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: (/ 1 8) + x1 + x2
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #2 #3 #18 #19 #21..23 #30 #32 #33 #41 #42 #47
Number of SCCs: 5, DPs: 0, edges: 0
YES