Input TRS:
    1: eq(0(),0()) -> true()
    2: eq(0(),s(x)) -> false()
    3: eq(s(x),0()) -> false()
    4: eq(s(x),s(y)) -> eq(x,y)
    5: or(true(),y) -> true()
    6: or(false(),y) -> y
    7: union(empty(),h) -> h
    8: union(edge(x,y,i),h) -> edge(x,y,union(i,h))
    9: isEmpty(empty()) -> true()
    10: isEmpty(edge(x,y,i)) -> false()
    11: from(edge(x,y,i)) -> x
    12: to(edge(x,y,i)) -> y
    13: rest(edge(x,y,i)) -> i
    14: rest(empty()) -> empty()
    15: reach(x,y,i,h) -> if1(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h)
    16: if1(true(),b1,b2,b3,x,y,i,h) -> true()
    17: if1(false(),b1,b2,b3,x,y,i,h) -> if2(b1,b2,b3,x,y,i,h)
    18: if2(true(),b2,b3,x,y,i,h) -> false()
    19: if2(false(),b2,b3,x,y,i,h) -> if3(b2,b3,x,y,i,h)
    20: if3(false(),b3,x,y,i,h) -> reach(x,y,rest(i),edge(from(i),to(i),h))
    21: if3(true(),b3,x,y,i,h) -> if4(b3,x,y,i,h)
    22: if4(true(),x,y,i,h) -> true()
    23: if4(false(),x,y,i,h) -> or(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty()))
Number of strict rules: 23
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #if4(false(),x,y,i,h) -> #or(reach(x,y,rest(i),h),reach(to(i),y,union(rest(i),h),empty()))
   #2: #if4(false(),x,y,i,h) -> #reach(x,y,rest(i),h)
   #3: #if4(false(),x,y,i,h) -> #rest(i)
   #4: #if4(false(),x,y,i,h) -> #reach(to(i),y,union(rest(i),h),empty())
   #5: #if4(false(),x,y,i,h) -> #to(i)
   #6: #if4(false(),x,y,i,h) -> #union(rest(i),h)
   #7: #if4(false(),x,y,i,h) -> #rest(i)
   #8: #if3(false(),b3,x,y,i,h) -> #reach(x,y,rest(i),edge(from(i),to(i),h))
   #9: #if3(false(),b3,x,y,i,h) -> #rest(i)
   #10: #if3(false(),b3,x,y,i,h) -> #from(i)
   #11: #if3(false(),b3,x,y,i,h) -> #to(i)
   #12: #if1(false(),b1,b2,b3,x,y,i,h) -> #if2(b1,b2,b3,x,y,i,h)
   #13: #if2(false(),b2,b3,x,y,i,h) -> #if3(b2,b3,x,y,i,h)
   #14: #if3(true(),b3,x,y,i,h) -> #if4(b3,x,y,i,h)
   #15: #union(edge(x,y,i),h) -> #union(i,h)
   #16: #reach(x,y,i,h) -> #if1(eq(x,y),isEmpty(i),eq(x,from(i)),eq(y,to(i)),x,y,i,h)
   #17: #reach(x,y,i,h) -> #eq(x,y)
   #18: #reach(x,y,i,h) -> #isEmpty(i)
   #19: #reach(x,y,i,h) -> #eq(x,from(i))
   #20: #reach(x,y,i,h) -> #from(i)
   #21: #reach(x,y,i,h) -> #eq(y,to(i))
   #22: #reach(x,y,i,h) -> #to(i)
   #23: #eq(s(x),s(y)) -> #eq(x,y)
Number of SCCs: 3, DPs: 9, edges: 11
	SCC { #23 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #if4(x1,x2,x3,x4,x5)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#rest(x1)	weight: 0
  edge(x1,x2,x3)	weight: 0
#isEmpty(x1)	weight: 0
    eq(x1,x2)	weight: 0
   if1(x1,x2,x3,x4,x5,x6,x7,x8)	weight: 0
 false()	weight: 0
isEmpty(x1)	weight: 0
  #to(x1)	weight: 0
 reach(x1,x2,x3,x4)	weight: 0
  true()	weight: 0
#reach(x1,x2,x3,x4)	weight: 0
  #eq(x1,x2)	weight: x2
 #if1(x1,x2,x3,x4,x5,x6,x7,x8)	weight: 0
   if2(x1,x2,x3,x4,x5,x6,x7)	weight: 0
 #if3(x1,x2,x3,x4,x5,x6)	weight: 0
     0()	weight: 0
  from(x1)	weight: 0
 union(x1,x2)	weight: 0
    or(x1,x2)	weight: 0
   if4(x1,x2,x3,x4,x5)	weight: 0
  rest(x1)	weight: 0
#from(x1)	weight: 0
   if3(x1,x2,x3,x4,x5,x6)	weight: 0
 empty()	weight: 0
  #or(x1,x2)	weight: 0
    to(x1)	weight: 0
 #if2(x1,x2,x3,x4,x5,x6,x7)	weight: 0
#union(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #23
Number of SCCs: 2, DPs: 8, edges: 10
	SCC { #15 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #if4(x1,x2,x3,x4,x5)	weight: 0
     s(x1)	weight: (/ 1 2)
#rest(x1)	weight: 0
  edge(x1,x2,x3)	weight: (/ 1 2) + x3
#isEmpty(x1)	weight: 0
    eq(x1,x2)	weight: 0
   if1(x1,x2,x3,x4,x5,x6,x7,x8)	weight: 0
 false()	weight: 0
isEmpty(x1)	weight: 0
  #to(x1)	weight: 0
 reach(x1,x2,x3,x4)	weight: 0
  true()	weight: 0
#reach(x1,x2,x3,x4)	weight: 0
  #eq(x1,x2)	weight: 0
 #if1(x1,x2,x3,x4,x5,x6,x7,x8)	weight: 0
   if2(x1,x2,x3,x4,x5,x6,x7)	weight: 0
 #if3(x1,x2,x3,x4,x5,x6)	weight: 0
     0()	weight: 0
  from(x1)	weight: 0
 union(x1,x2)	weight: 0
    or(x1,x2)	weight: 0
   if4(x1,x2,x3,x4,x5)	weight: 0
  rest(x1)	weight: 0
#from(x1)	weight: 0
   if3(x1,x2,x3,x4,x5,x6)	weight: 0
 empty()	weight: 0
  #or(x1,x2)	weight: 0
    to(x1)	weight: 0
 #if2(x1,x2,x3,x4,x5,x6,x7)	weight: 0
#union(x1,x2)	weight: x1
    Usable rules: { }
    Removed DPs: #15
Number of SCCs: 1, DPs: 7, edges: 9
	SCC { #2 #4 #8 #12..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