Input TRS:
    1: a__minus(0(),Y) -> 0()
    2: a__minus(s(X),s(Y)) -> a__minus(X,Y)
    3: a__geq(X,0()) -> true()
    4: a__geq(0(),s(Y)) -> false()
    5: a__geq(s(X),s(Y)) -> a__geq(X,Y)
    6: a__div(0(),s(Y)) -> 0()
    7: a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    8: a__if(true(),X,Y) -> mark(X)
    9: a__if(false(),X,Y) -> mark(Y)
    10: mark(minus(X1,X2)) -> a__minus(X1,X2)
    11: mark(geq(X1,X2)) -> a__geq(X1,X2)
    12: mark(div(X1,X2)) -> a__div(mark(X1),X2)
    13: mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
    14: mark(0()) -> 0()
    15: mark(s(X)) -> s(mark(X))
    16: mark(true()) -> true()
    17: mark(false()) -> false()
    18: a__minus(X1,X2) -> minus(X1,X2)
    19: a__geq(X1,X2) -> geq(X1,X2)
    20: a__div(X1,X2) -> div(X1,X2)
    21: a__if(X1,X2,X3) -> if(X1,X2,X3)
Number of strict rules: 21
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #a__minus(s(X),s(Y)) -> #a__minus(X,Y)
   #2: #mark(if(X1,X2,X3)) -> #a__if(mark(X1),X2,X3)
   #3: #mark(if(X1,X2,X3)) -> #mark(X1)
   #4: #a__if(false(),X,Y) -> #mark(Y)
   #5: #mark(geq(X1,X2)) -> #a__geq(X1,X2)
   #6: #mark(div(X1,X2)) -> #a__div(mark(X1),X2)
   #7: #mark(div(X1,X2)) -> #mark(X1)
   #8: #a__div(s(X),s(Y)) -> #a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
   #9: #a__div(s(X),s(Y)) -> #a__geq(X,Y)
   #10: #mark(minus(X1,X2)) -> #a__minus(X1,X2)
   #11: #a__geq(s(X),s(Y)) -> #a__geq(X,Y)
   #12: #a__if(true(),X,Y) -> #mark(X)
   #13: #mark(s(X)) -> #mark(X)
Number of SCCs: 3, DPs: 10, edges: 32
	SCC { #1 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
a__minus(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
 minus(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
a__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
#a__minus(x1,x2)	weight: x2
a__geq(x1,x2)	weight: 0
  mark(x1)	weight: 0
#a__geq(x1,x2)	weight: 0
#a__if(x1,x2,x3)	weight: 0
#a__div(x1,x2)	weight: 0
 a__if(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #1
Number of SCCs: 2, DPs: 9, edges: 31
	SCC { #11 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
a__minus(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
 minus(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
a__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
#a__minus(x1,x2)	weight: 0
a__geq(x1,x2)	weight: 0
  mark(x1)	weight: 0
#a__geq(x1,x2)	weight: x2
#a__if(x1,x2,x3)	weight: 0
#a__div(x1,x2)	weight: 0
 a__if(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #11
Number of SCCs: 1, DPs: 8, edges: 30
	SCC { #2..4 #6..8 #12 #13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
a__minus(x1,x2)	weight: (/ 1 2) + x1
     s(x1)	weight: x1
 minus(x1,x2)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: (/ 1 4) + x1
a__div(x1,x2)	weight: (/ 3 4)
   geq(x1,x2)	weight: 0
  true()	weight: 0
#mark(x1)	weight: x1
     0()	weight: 0
    if(x1,x2,x3)	weight: (/ 1 4) + x1 + x2 + x3
#a__minus(x1,x2)	weight: 0
a__geq(x1,x2)	weight: (/ 1 2)
  mark(x1)	weight: (/ 1 4) + x1
#a__geq(x1,x2)	weight: 0
#a__if(x1,x2,x3)	weight: x2 + x3
#a__div(x1,x2)	weight: (/ 1 4)
 a__if(x1,x2,x3)	weight: 0
    Usable rules: { 3..5 19 }
    Removed DPs: #2 #3 #7
Number of SCCs: 1, DPs: 5, edges: 9
	SCC { #4 #6 #8 #12 #13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
a__minus(x1,x2)	weight: x1
     s(x1)	weight: (/ 1 4) + x1
 minus(x1,x2)	weight: x1
 false()	weight: 0
   div(x1,x2)	weight: (/ 1 4) + x1
a__div(x1,x2)	weight: (/ 1 4) + x1
   geq(x1,x2)	weight: (/ 1 4)
  true()	weight: 0
#mark(x1)	weight: x1
     0()	weight: 0
    if(x1,x2,x3)	weight: x2 + x3
#a__minus(x1,x2)	weight: 0
a__geq(x1,x2)	weight: (/ 1 4)
  mark(x1)	weight: x1
#a__geq(x1,x2)	weight: 0
#a__if(x1,x2,x3)	weight: x2 + x3
#a__div(x1,x2)	weight: (/ 1 4) + x1
 a__if(x1,x2,x3)	weight: x2 + x3
    Usable rules: { 1..21 }
    Removed DPs: #13
Number of SCCs: 1, DPs: 4, edges: 5
	SCC { #4 #6 #8 #12 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
a__minus(x1,x2)	weight: (/ 3 16) + x1
     s(x1)	weight: (/ 1 16)
 minus(x1,x2)	weight: (/ 1 16) + x2
 false()	weight: 0
   div(x1,x2)	weight: (/ 1 4)
a__div(x1,x2)	weight: (/ 3 8)
   geq(x1,x2)	weight: (/ 1 8)
  true()	weight: 0
#mark(x1)	weight: x1
     0()	weight: 0
    if(x1,x2,x3)	weight: (/ 1 2) + x2 + x3
#a__minus(x1,x2)	weight: 0
a__geq(x1,x2)	weight: (/ 1 16)
  mark(x1)	weight: (/ 1 16) + x1
#a__geq(x1,x2)	weight: 0
#a__if(x1,x2,x3)	weight: (/ 1 16) + x2 + x3
#a__div(x1,x2)	weight: (/ 3 16)
 a__if(x1,x2,x3)	weight: (/ 7 16)
    Usable rules: { }
    Removed DPs: #4 #6 #8 #12
Number of SCCs: 0, DPs: 0, edges: 0
YES