Input TRS:
    1: gcd(x,y) -> gcd2(x,y,0())
    2: gcd2(x,y,i) -> if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i))
    3: if1(true(),b1,b2,b3,x,y,i) -> pair(result(y),neededIterations(i))
    4: if1(false(),b1,b2,b3,x,y,i) -> if2(b1,b2,b3,x,y,i)
    5: if2(true(),b2,b3,x,y,i) -> pair(result(x),neededIterations(i))
    6: if2(false(),b2,b3,x,y,i) -> if3(b2,b3,x,y,i)
    7: if3(false(),b3,x,y,i) -> gcd2(minus(x,y),y,i)
    8: if3(true(),b3,x,y,i) -> if4(b3,x,y,i)
    9: if4(false(),x,y,i) -> gcd2(x,minus(y,x),i)
    10: if4(true(),x,y,i) -> pair(result(x),neededIterations(i))
    11: inc(0()) -> 0()
    12: inc(s(i)) -> s(inc(i))
    13: le(s(x),0()) -> false()
    14: le(0(),y) -> true()
    15: le(s(x),s(y)) -> le(x,y)
    16: minus(x,0()) -> x
    17: minus(0(),y) -> 0()
    18: minus(s(x),s(y)) -> minus(x,y)
    19: a() -> b()
    20: a() -> c()
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #gcd2(x,y,i) -> #if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i))
   #2: #gcd2(x,y,i) -> #le(x,0())
   #3: #gcd2(x,y,i) -> #le(y,0())
   #4: #gcd2(x,y,i) -> #le(x,y)
   #5: #gcd2(x,y,i) -> #le(y,x)
   #6: #gcd2(x,y,i) -> #inc(i)
   #7: #if2(false(),b2,b3,x,y,i) -> #if3(b2,b3,x,y,i)
   #8: #if4(false(),x,y,i) -> #gcd2(x,minus(y,x),i)
   #9: #if4(false(),x,y,i) -> #minus(y,x)
   #10: #inc(s(i)) -> #inc(i)
   #11: #if3(false(),b3,x,y,i) -> #gcd2(minus(x,y),y,i)
   #12: #if3(false(),b3,x,y,i) -> #minus(x,y)
   #13: #gcd(x,y) -> #gcd2(x,y,0())
   #14: #if3(true(),b3,x,y,i) -> #if4(b3,x,y,i)
   #15: #le(s(x),s(y)) -> #le(x,y)
   #16: #if1(false(),b1,b2,b3,x,y,i) -> #if2(b1,b2,b3,x,y,i)
   #17: #minus(s(x),s(y)) -> #minus(x,y)
Number of SCCs: 4, DPs: 9, edges: 10
	SCC { #10 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
    le(x1,x2)	weight: 0
 #if4(x1,x2,x3,x4)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: 0
result(x1)	weight: 0
     b()	weight: 0
 minus(x1,x2)	weight: 0
   gcd(x1,x2)	weight: 0
   if1(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  pair(x1,x2)	weight: 0
 false()	weight: 0
 #inc(x1)	weight: x1
     c()	weight: 0
   inc(x1)	weight: 0
  true()	weight: 0
 #if1(x1,x2,x3,x4,x5,x6,x7)	weight: 0
   if2(x1,x2,x3,x4,x5,x6)	weight: 0
 #if3(x1,x2,x3,x4,x5)	weight: 0
     0()	weight: 0
#gcd2(x1,x2,x3)	weight: 0
neededIterations(x1)	weight: 0
  gcd2(x1,x2,x3)	weight: 0
   if4(x1,x2,x3,x4)	weight: 0
#minus(x1,x2)	weight: 0
   if3(x1,x2,x3,x4,x5)	weight: 0
   #a()	weight: 0
 #if2(x1,x2,x3,x4,x5,x6)	weight: 0
 #gcd(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #10
Number of SCCs: 3, DPs: 8, edges: 9
	SCC { #17 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
    le(x1,x2)	weight: 0
 #if4(x1,x2,x3,x4)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: 0
result(x1)	weight: 0
     b()	weight: 0
 minus(x1,x2)	weight: 0
   gcd(x1,x2)	weight: 0
   if1(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  pair(x1,x2)	weight: 0
 false()	weight: 0
 #inc(x1)	weight: 0
     c()	weight: 0
   inc(x1)	weight: 0
  true()	weight: 0
 #if1(x1,x2,x3,x4,x5,x6,x7)	weight: 0
   if2(x1,x2,x3,x4,x5,x6)	weight: 0
 #if3(x1,x2,x3,x4,x5)	weight: 0
     0()	weight: 0
#gcd2(x1,x2,x3)	weight: 0
neededIterations(x1)	weight: 0
  gcd2(x1,x2,x3)	weight: 0
   if4(x1,x2,x3,x4)	weight: 0
#minus(x1,x2)	weight: x2
   if3(x1,x2,x3,x4,x5)	weight: 0
   #a()	weight: 0
 #if2(x1,x2,x3,x4,x5,x6)	weight: 0
 #gcd(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #17
Number of SCCs: 2, DPs: 7, edges: 8
	SCC { #15 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
    le(x1,x2)	weight: 0
 #if4(x1,x2,x3,x4)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: x2
result(x1)	weight: 0
     b()	weight: 0
 minus(x1,x2)	weight: 0
   gcd(x1,x2)	weight: 0
   if1(x1,x2,x3,x4,x5,x6,x7)	weight: 0
  pair(x1,x2)	weight: 0
 false()	weight: 0
 #inc(x1)	weight: 0
     c()	weight: 0
   inc(x1)	weight: 0
  true()	weight: 0
 #if1(x1,x2,x3,x4,x5,x6,x7)	weight: 0
   if2(x1,x2,x3,x4,x5,x6)	weight: 0
 #if3(x1,x2,x3,x4,x5)	weight: 0
     0()	weight: 0
#gcd2(x1,x2,x3)	weight: 0
neededIterations(x1)	weight: 0
  gcd2(x1,x2,x3)	weight: 0
   if4(x1,x2,x3,x4)	weight: 0
#minus(x1,x2)	weight: 0
   if3(x1,x2,x3,x4,x5)	weight: 0
   #a()	weight: 0
 #if2(x1,x2,x3,x4,x5,x6)	weight: 0
 #gcd(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #15
Number of SCCs: 1, DPs: 6, edges: 7
	SCC { #1 #7 #8 #11 #14 #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