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: and(true(),y) -> y
    8: and(false(),y) -> false()
    9: size(empty()) -> 0()
    10: size(edge(x,y,i)) -> s(size(i))
    11: le(0(),y) -> true()
    12: le(s(x),0()) -> false()
    13: le(s(x),s(y)) -> le(x,y)
    14: reachable(x,y,i) -> reach(x,y,0(),i,i)
    15: reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
    16: if1(true(),x,y,c,i,j) -> true()
    17: if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
    18: if2(false(),x,y,c,i,j) -> false()
    19: if2(true(),x,y,c,empty(),j) -> false()
    20: if2(true(),x,y,c,edge(u,v,i),j) -> or(if2(true(),x,y,c,i,j),and(eq(x,u),reach(v,y,s(c),j,j)))
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... failed.
Freezing if2
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: and(true(),y) -> y
8: and(false(),y) -> false()
9: size(empty()) -> 0()
10: size(edge(x,y,i)) -> s(size(i))
11: le(0(),y) -> true()
12: le(s(x),0()) -> false()
13: le(s(x),s(y)) -> le(x,y)
14: reachable(x,y,i) -> reach(x,y,0(),i,i)
15: reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
16: if1(true(),x,y,c,i,j) -> true()
17: if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
18: if2❆1_false(x,y,c,i,j) -> false()
19: if2❆1_true(x,y,c,empty(),j) -> false()
20: if2❆1_true(x,y,c,edge(u,v,i),j) -> or(if2❆1_true(x,y,c,i,j),and(eq(x,u),reach(v,y,s(c),j,j)))
21: if2(false(),_5,_6,_7,_8,_9) ->= if2❆1_false(_5,_6,_7,_8,_9)
22: if2(true(),_5,_6,_7,_8,_9) ->= if2❆1_true(_5,_6,_7,_8,_9)
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #le(s(x),s(y)) -> #le(x,y)
   #2: #reachable(x,y,i) -> #reach(x,y,0(),i,i)
   #3: #if2❆1_true(x,y,c,edge(u,v,i),j) -> #or(if2❆1_true(x,y,c,i,j),and(eq(x,u),reach(v,y,s(c),j,j)))
   #4: #if2❆1_true(x,y,c,edge(u,v,i),j) -> #if2❆1_true(x,y,c,i,j)
   #5: #if2❆1_true(x,y,c,edge(u,v,i),j) -> #and(eq(x,u),reach(v,y,s(c),j,j))
   #6: #if2❆1_true(x,y,c,edge(u,v,i),j) -> #eq(x,u)
   #7: #if2❆1_true(x,y,c,edge(u,v,i),j) -> #reach(v,y,s(c),j,j)
   #8: #size(edge(x,y,i)) -> #size(i)
   #9: #if2(true(),_5,_6,_7,_8,_9) ->? #if2❆1_true(_5,_6,_7,_8,_9)
   #10: #if1(false(),x,y,c,i,j) -> #if2(le(c,size(j)),x,y,c,i,j)
   #11: #if1(false(),x,y,c,i,j) -> #le(c,size(j))
   #12: #if1(false(),x,y,c,i,j) -> #size(j)
   #13: #if2(false(),_5,_6,_7,_8,_9) ->? #if2❆1_false(_5,_6,_7,_8,_9)
   #14: #reach(x,y,c,i,j) -> #if1(eq(x,y),x,y,c,i,j)
   #15: #reach(x,y,c,i,j) -> #eq(x,y)
   #16: #eq(s(x),s(y)) -> #eq(x,y)
Number of SCCs: 4, DPs: 8, edges: 10
	SCC { #8 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
    le(x1,x2)	weight: 0
     s(x1)	weight: 0
  #le(x1,x2)	weight: 0
  edge(x1,x2,x3)	weight: (/ 1 2) + x3
   and(x1,x2)	weight: 0
    eq(x1,x2)	weight: 0
   if1(x1,x2,x3,x4,x5,x6)	weight: 0
 false()	weight: 0
#reachable(x1,x2,x3)	weight: 0
#if2❆1_true(x1,x2,x3,x4,x5)	weight: 0
 reach(x1,x2,x3,x4,x5)	weight: 0
  true()	weight: 0
reachable(x1,x2,x3)	weight: 0
#reach(x1,x2,x3,x4,x5)	weight: 0
  #eq(x1,x2)	weight: 0
 #if1(x1,x2,x3,x4,x5,x6)	weight: 0
#size(x1)	weight: x1
   if2(x1,x2,x3,x4,x5,x6)	weight: 0
if2❆1_true(x1,x2,x3,x4,x5)	weight: 0
     0()	weight: 0
    or(x1,x2)	weight: 0
 empty()	weight: 0
#if2❆1_false(x1,x2,x3,x4,x5)	weight: 0
  #or(x1,x2)	weight: 0
 #if2(x1,x2,x3,x4,x5,x6)	weight: 0
 #and(x1,x2)	weight: 0
  size(x1)	weight: 0
if2❆1_false(x1,x2,x3,x4,x5)	weight: 0
    Usable rules: { }
    Removed DPs: #8
Number of SCCs: 3, DPs: 7, edges: 9
	SCC { #16 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
    le(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: 0
  edge(x1,x2,x3)	weight: (/ 1 2)
   and(x1,x2)	weight: 0
    eq(x1,x2)	weight: 0
   if1(x1,x2,x3,x4,x5,x6)	weight: 0
 false()	weight: 0
#reachable(x1,x2,x3)	weight: 0
#if2❆1_true(x1,x2,x3,x4,x5)	weight: 0
 reach(x1,x2,x3,x4,x5)	weight: 0
  true()	weight: 0
reachable(x1,x2,x3)	weight: 0
#reach(x1,x2,x3,x4,x5)	weight: 0
  #eq(x1,x2)	weight: x2
 #if1(x1,x2,x3,x4,x5,x6)	weight: 0
#size(x1)	weight: 0
   if2(x1,x2,x3,x4,x5,x6)	weight: 0
if2❆1_true(x1,x2,x3,x4,x5)	weight: 0
     0()	weight: 0
    or(x1,x2)	weight: 0
 empty()	weight: 0
#if2❆1_false(x1,x2,x3,x4,x5)	weight: 0
  #or(x1,x2)	weight: 0
 #if2(x1,x2,x3,x4,x5,x6)	weight: 0
 #and(x1,x2)	weight: 0
  size(x1)	weight: 0
if2❆1_false(x1,x2,x3,x4,x5)	weight: 0
    Usable rules: { }
    Removed DPs: #16
Number of SCCs: 2, DPs: 6, edges: 8
	SCC { #1 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
    le(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: x2
  edge(x1,x2,x3)	weight: (/ 1 2)
   and(x1,x2)	weight: 0
    eq(x1,x2)	weight: 0
   if1(x1,x2,x3,x4,x5,x6)	weight: 0
 false()	weight: 0
#reachable(x1,x2,x3)	weight: 0
#if2❆1_true(x1,x2,x3,x4,x5)	weight: 0
 reach(x1,x2,x3,x4,x5)	weight: 0
  true()	weight: 0
reachable(x1,x2,x3)	weight: 0
#reach(x1,x2,x3,x4,x5)	weight: 0
  #eq(x1,x2)	weight: 0
 #if1(x1,x2,x3,x4,x5,x6)	weight: 0
#size(x1)	weight: 0
   if2(x1,x2,x3,x4,x5,x6)	weight: 0
if2❆1_true(x1,x2,x3,x4,x5)	weight: 0
     0()	weight: 0
    or(x1,x2)	weight: 0
 empty()	weight: 0
#if2❆1_false(x1,x2,x3,x4,x5)	weight: 0
  #or(x1,x2)	weight: 0
 #if2(x1,x2,x3,x4,x5,x6)	weight: 0
 #and(x1,x2)	weight: 0
  size(x1)	weight: 0
if2❆1_false(x1,x2,x3,x4,x5)	weight: 0
    Usable rules: { }
    Removed DPs: #1
Number of SCCs: 1, DPs: 5, edges: 7
	SCC { #4 #7 #9 #10 #14 }
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