Input TRS:
    1: active(minus(0(),Y)) -> mark(0())
    2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
    3: active(geq(X,0())) -> mark(true())
    4: active(geq(0(),s(Y))) -> mark(false())
    5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
    6: active(div(0(),s(Y))) -> mark(0())
    7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
    8: active(if(true(),X,Y)) -> mark(X)
    9: active(if(false(),X,Y)) -> mark(Y)
    10: mark(minus(X1,X2)) -> active(minus(X1,X2))
    11: mark(0()) -> active(0())
    12: mark(s(X)) -> active(s(mark(X)))
    13: mark(geq(X1,X2)) -> active(geq(X1,X2))
    14: mark(true()) -> active(true())
    15: mark(false()) -> active(false())
    16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
    17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
    18: minus(mark(X1),X2) -> minus(X1,X2)
    19: minus(X1,mark(X2)) -> minus(X1,X2)
    20: minus(active(X1),X2) -> minus(X1,X2)
    21: minus(X1,active(X2)) -> minus(X1,X2)
    22: s(mark(X)) -> s(X)
    23: s(active(X)) -> s(X)
    24: geq(mark(X1),X2) -> geq(X1,X2)
    25: geq(X1,mark(X2)) -> geq(X1,X2)
    26: geq(active(X1),X2) -> geq(X1,X2)
    27: geq(X1,active(X2)) -> geq(X1,X2)
    28: div(mark(X1),X2) -> div(X1,X2)
    29: div(X1,mark(X2)) -> div(X1,X2)
    30: div(active(X1),X2) -> div(X1,X2)
    31: div(X1,active(X2)) -> div(X1,X2)
    32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
    33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
    34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
    35: if(active(X1),X2,X3) -> if(X1,X2,X3)
    36: if(X1,active(X2),X3) -> if(X1,X2,X3)
    37: if(X1,X2,active(X3)) -> if(X1,X2,X3)
Number of strict rules: 37
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(minus(s(X),s(Y))) -> #mark(minus(X,Y))
   #2: #active(minus(s(X),s(Y))) -> #minus(X,Y)
   #3: #div(X1,mark(X2)) -> #div(X1,X2)
   #4: #if(active(X1),X2,X3) -> #if(X1,X2,X3)
   #5: #if(X1,X2,active(X3)) -> #if(X1,X2,X3)
   #6: #active(div(0(),s(Y))) -> #mark(0())
   #7: #mark(geq(X1,X2)) -> #active(geq(X1,X2))
   #8: #active(if(false(),X,Y)) -> #mark(Y)
   #9: #mark(0()) -> #active(0())
   #10: #geq(mark(X1),X2) -> #geq(X1,X2)
   #11: #s(active(X)) -> #s(X)
   #12: #mark(s(X)) -> #active(s(mark(X)))
   #13: #mark(s(X)) -> #s(mark(X))
   #14: #mark(s(X)) -> #mark(X)
   #15: #div(X1,active(X2)) -> #div(X1,X2)
   #16: #mark(true()) -> #active(true())
   #17: #div(active(X1),X2) -> #div(X1,X2)
   #18: #geq(X1,mark(X2)) -> #geq(X1,X2)
   #19: #minus(active(X1),X2) -> #minus(X1,X2)
   #20: #active(div(s(X),s(Y))) -> #mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0()))
   #21: #active(div(s(X),s(Y))) -> #if(geq(X,Y),s(div(minus(X,Y),s(Y))),0())
   #22: #active(div(s(X),s(Y))) -> #geq(X,Y)
   #23: #active(div(s(X),s(Y))) -> #s(div(minus(X,Y),s(Y)))
   #24: #active(div(s(X),s(Y))) -> #div(minus(X,Y),s(Y))
   #25: #active(div(s(X),s(Y))) -> #minus(X,Y)
   #26: #mark(minus(X1,X2)) -> #active(minus(X1,X2))
   #27: #if(X1,mark(X2),X3) -> #if(X1,X2,X3)
   #28: #active(geq(s(X),s(Y))) -> #mark(geq(X,Y))
   #29: #active(geq(s(X),s(Y))) -> #geq(X,Y)
   #30: #div(mark(X1),X2) -> #div(X1,X2)
   #31: #s(mark(X)) -> #s(X)
   #32: #if(X1,X2,mark(X3)) -> #if(X1,X2,X3)
   #33: #geq(X1,active(X2)) -> #geq(X1,X2)
   #34: #mark(if(X1,X2,X3)) -> #active(if(mark(X1),X2,X3))
   #35: #mark(if(X1,X2,X3)) -> #if(mark(X1),X2,X3)
   #36: #mark(if(X1,X2,X3)) -> #mark(X1)
   #37: #if(mark(X1),X2,X3) -> #if(X1,X2,X3)
   #38: #minus(X1,mark(X2)) -> #minus(X1,X2)
   #39: #geq(active(X1),X2) -> #geq(X1,X2)
   #40: #if(X1,active(X2),X3) -> #if(X1,X2,X3)
   #41: #minus(X1,active(X2)) -> #minus(X1,X2)
   #42: #mark(div(X1,X2)) -> #active(div(mark(X1),X2))
   #43: #mark(div(X1,X2)) -> #div(mark(X1),X2)
   #44: #mark(div(X1,X2)) -> #mark(X1)
   #45: #active(geq(X,0())) -> #mark(true())
   #46: #active(minus(0(),Y)) -> #mark(0())
   #47: #active(if(true(),X,Y)) -> #mark(X)
   #48: #mark(false()) -> #active(false())
   #49: #active(geq(0(),s(Y))) -> #mark(false())
   #50: #minus(mark(X1),X2) -> #minus(X1,X2)
Number of SCCs: 8, DPs: 32, edges: 122
	SCC { #11 #31 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: 0
     s(x1)	weight: 0
 minus(x1,x2)	weight: 0
 #geq(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
   geq(x1,x2)	weight: 0
  true()	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   #s(x1)	weight: x1
  mark(x1)	weight: (/ 1 2) + x1
#minus(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #11 #31
Number of SCCs: 7, DPs: 30, edges: 118
	SCC { #1 #26 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
 minus(x1,x2)	weight: (/ 1 4) + x1
 #geq(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
   geq(x1,x2)	weight: 0
  true()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#minus(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: x1
    Usable rules: { 18..21 }
    Removed DPs: #1 #26
Number of SCCs: 6, DPs: 28, edges: 116
	SCC { #7 #28 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
 minus(x1,x2)	weight: (/ 1 4) + x1
 #geq(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
   geq(x1,x2)	weight: (/ 1 4) + x1
  true()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#minus(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: x1
    Usable rules: { 24..27 }
    Removed DPs: #7 #28
Number of SCCs: 5, DPs: 26, edges: 114
	SCC { #3 #15 #17 #30 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: x1
     s(x1)	weight: (/ 1 2)
 minus(x1,x2)	weight: (/ 1 4) + x1
 #geq(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
   geq(x1,x2)	weight: (/ 1 4) + x1
  true()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#minus(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #17 #30
Number of SCCs: 5, DPs: 24, edges: 102
	SCC { #3 #15 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: x2
     s(x1)	weight: (/ 1 2)
 minus(x1,x2)	weight: (/ 1 4) + x1
 #geq(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
   geq(x1,x2)	weight: (/ 1 4) + x1
  true()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#minus(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #3 #15
Number of SCCs: 4, DPs: 22, edges: 98
	SCC { #19 #38 #41 #50 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2)
 minus(x1,x2)	weight: (/ 1 4) + x1
 #geq(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
   geq(x1,x2)	weight: (/ 1 4) + x1
  true()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#minus(x1,x2)	weight: x1
active(x1)	weight: (/ 1 4) + x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #19 #50
Number of SCCs: 5, DPs: 20, edges: 86
	SCC { #38 #41 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2)
 minus(x1,x2)	weight: (/ 1 4) + x1
 #geq(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
   geq(x1,x2)	weight: (/ 1 4) + x1
  true()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#minus(x1,x2)	weight: x2
active(x1)	weight: (/ 1 4) + x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #38 #41
Number of SCCs: 4, DPs: 18, edges: 82
	SCC { #10 #18 #33 #39 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2)
 minus(x1,x2)	weight: (/ 1 4) + x1
 #geq(x1,x2)	weight: x2
 false()	weight: 0
   div(x1,x2)	weight: 0
   geq(x1,x2)	weight: (/ 1 4) + x1
  true()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#minus(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #18 #33
Number of SCCs: 5, DPs: 16, edges: 70
	SCC { #10 #39 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2)
 minus(x1,x2)	weight: (/ 1 4) + x1
 #geq(x1,x2)	weight: x1
 false()	weight: 0
   div(x1,x2)	weight: 0
   geq(x1,x2)	weight: (/ 1 4) + x1
  true()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#minus(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #10 #39
Number of SCCs: 4, DPs: 14, edges: 66
	SCC { #4 #5 #27 #32 #37 #40 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2)
 minus(x1,x2)	weight: (/ 1 4) + x1
 #geq(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
   geq(x1,x2)	weight: (/ 1 4) + x1
  true()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#minus(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  #if(x1,x2,x3)	weight: x1 + x3
#active(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #4 #5 #32 #37
Number of SCCs: 5, DPs: 10, edges: 34
	SCC { #27 #40 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2)
 minus(x1,x2)	weight: (/ 1 4) + x1
 #geq(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
   geq(x1,x2)	weight: (/ 1 4) + x1
  true()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   #s(x1)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#minus(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  #if(x1,x2,x3)	weight: x2
#active(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #27 #40
Number of SCCs: 4, DPs: 8, edges: 30
	SCC { #8 #14 #20 #34 #36 #42 #44 #47 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
 minus(x1,x2)	weight: 0
 #geq(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: (/ 1 4) + x1
   geq(x1,x2)	weight: x1
  true()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: x1 + x2 + x3
   #s(x1)	weight: 0
  mark(x1)	weight: x1
#minus(x1,x2)	weight: 0
active(x1)	weight: x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: (/ 1 4) + x1
    Usable rules: { 1..37 }
    Removed DPs: #14 #44
Number of SCCs: 5, DPs: 6, edges: 14
	SCC { #8 #20 #34 #36 #42 #47 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #div(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8)
 minus(x1,x2)	weight: (/ 1 8)
 #geq(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: (/ 3 4)
   geq(x1,x2)	weight: (/ 1 8)
  true()	weight: 0
#mark(x1)	weight: (/ 1 8) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: (/ 1 4) + x1 + x2 + x3
   #s(x1)	weight: 0
  mark(x1)	weight: x1
#minus(x1,x2)	weight: 0
active(x1)	weight: x1
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: x1
    Usable rules: { 1..37 }
    Removed DPs: #8 #20 #34 #36 #42 #47
Number of SCCs: 4, DPs: 0, edges: 0
YES