Input TRS:
    1: div(x,y) -> div2(x,y,0())
    2: div2(x,y,i) -> if1(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i))
    3: if1(true(),b,x,y,i,j) -> divZeroError()
    4: if1(false(),b,x,y,i,j) -> if2(b,x,y,i,j)
    5: if2(true(),x,y,i,j) -> div2(minus(x,y),y,j)
    6: if2(false(),x,y,i,j) -> i
    7: inc(0()) -> 0()
    8: inc(s(i)) -> s(inc(i))
    9: le(s(x),0()) -> false()
    10: le(0(),y) -> true()
    11: le(s(x),s(y)) -> le(x,y)
    12: minus(x,0()) -> x
    13: minus(0(),y) -> 0()
    14: minus(s(x),s(y)) -> minus(x,y)
    15: plus(x,y) -> plusIter(x,y,0())
    16: plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
    17: ifPlus(true(),x,y,z) -> y
    18: ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
    19: a() -> c()
    20: a() -> d()
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #div2(x,y,i) -> #if1(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i))
   #2: #div2(x,y,i) -> #le(y,0())
   #3: #div2(x,y,i) -> #le(y,x)
   #4: #div2(x,y,i) -> #plus(i,0())
   #5: #div2(x,y,i) -> #inc(i)
   #6: #le(s(x),s(y)) -> #le(x,y)
   #7: #minus(s(x),s(y)) -> #minus(x,y)
   #8: #if2(true(),x,y,i,j) -> #div2(minus(x,y),y,j)
   #9: #if2(true(),x,y,i,j) -> #minus(x,y)
   #10: #plusIter(x,y,z) -> #ifPlus(le(x,z),x,y,z)
   #11: #plusIter(x,y,z) -> #le(x,z)
   #12: #div(x,y) -> #div2(x,y,0())
   #13: #inc(s(i)) -> #inc(i)
   #14: #plus(x,y) -> #plusIter(x,y,0())
   #15: #if1(false(),b,x,y,i,j) -> #if2(b,x,y,i,j)
   #16: #ifPlus(false(),x,y,z) -> #plusIter(x,s(y),s(z))
Number of SCCs: 5, DPs: 8, edges: 8
	SCC { #13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
    le(x1,x2)	weight: 0
plusIter(x1,x2,x3)	weight: 0
 #div(x1,x2)	weight: 0
     d()	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: 0
 minus(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
   if1(x1,x2,x3,x4,x5,x6)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
 #inc(x1)	weight: x1
     c()	weight: 0
   inc(x1)	weight: 0
  true()	weight: 0
 #if1(x1,x2,x3,x4,x5,x6)	weight: 0
   if2(x1,x2,x3,x4,x5)	weight: 0
     0()	weight: 0
  div2(x1,x2,x3)	weight: 0
divZeroError()	weight: 0
#div2(x1,x2,x3)	weight: 0
#minus(x1,x2)	weight: 0
ifPlus(x1,x2,x3,x4)	weight: 0
  plus(x1,x2)	weight: 0
   #a()	weight: 0
#ifPlus(x1,x2,x3,x4)	weight: 0
 #if2(x1,x2,x3,x4,x5)	weight: 0
#plusIter(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #13
Number of SCCs: 4, DPs: 7, edges: 7
	SCC { #7 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
    le(x1,x2)	weight: 0
plusIter(x1,x2,x3)	weight: 0
 #div(x1,x2)	weight: 0
     d()	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: 0
 minus(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
   if1(x1,x2,x3,x4,x5,x6)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
 #inc(x1)	weight: 0
     c()	weight: 0
   inc(x1)	weight: 0
  true()	weight: 0
 #if1(x1,x2,x3,x4,x5,x6)	weight: 0
   if2(x1,x2,x3,x4,x5)	weight: 0
     0()	weight: 0
  div2(x1,x2,x3)	weight: 0
divZeroError()	weight: 0
#div2(x1,x2,x3)	weight: 0
#minus(x1,x2)	weight: x2
ifPlus(x1,x2,x3,x4)	weight: 0
  plus(x1,x2)	weight: 0
   #a()	weight: 0
#ifPlus(x1,x2,x3,x4)	weight: 0
 #if2(x1,x2,x3,x4,x5)	weight: 0
#plusIter(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #7
Number of SCCs: 3, DPs: 6, edges: 6
	SCC { #6 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
    le(x1,x2)	weight: 0
plusIter(x1,x2,x3)	weight: 0
 #div(x1,x2)	weight: 0
     d()	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: x2
 minus(x1,x2)	weight: 0
#plus(x1,x2)	weight: 0
   if1(x1,x2,x3,x4,x5,x6)	weight: 0
 false()	weight: 0
   div(x1,x2)	weight: 0
 #inc(x1)	weight: 0
     c()	weight: 0
   inc(x1)	weight: 0
  true()	weight: 0
 #if1(x1,x2,x3,x4,x5,x6)	weight: 0
   if2(x1,x2,x3,x4,x5)	weight: 0
     0()	weight: 0
  div2(x1,x2,x3)	weight: 0
divZeroError()	weight: 0
#div2(x1,x2,x3)	weight: 0
#minus(x1,x2)	weight: 0
ifPlus(x1,x2,x3,x4)	weight: 0
  plus(x1,x2)	weight: 0
   #a()	weight: 0
#ifPlus(x1,x2,x3,x4)	weight: 0
 #if2(x1,x2,x3,x4,x5)	weight: 0
#plusIter(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #6
Number of SCCs: 2, DPs: 5, edges: 5
	SCC { #10 #16 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed.
Removing edges: failed.
Finding a loop...  failed.
MAYBE