MAYBE

Problem:
 eq(0(),0()) -> true()
 eq(0(),s(x)) -> false()
 eq(s(x),0()) -> false()
 eq(s(x),s(y)) -> eq(x,y)
 or(true(),y) -> true()
 or(false(),y) -> y
 and(true(),y) -> y
 and(false(),y) -> false()
 size(empty()) -> 0()
 size(edge(x,y,i)) -> s(size(i))
 le(0(),y) -> true()
 le(s(x),0()) -> false()
 le(s(x),s(y)) -> le(x,y)
 reachable(x,y,i) -> reach(x,y,0(),i,i)
 reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
 if1(true(),x,y,c,i,j) -> true()
 if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
 if2(false(),x,y,c,i,j) -> false()
 if2(true(),x,y,c,empty(),j) -> false()
 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)))

Proof:
 DP Processor:
  DPs:
   eq#(s(x),s(y)) -> eq#(x,y)
   size#(edge(x,y,i)) -> size#(i)
   le#(s(x),s(y)) -> le#(x,y)
   reachable#(x,y,i) -> reach#(x,y,0(),i,i)
   reach#(x,y,c,i,j) -> eq#(x,y)
   reach#(x,y,c,i,j) -> if1#(eq(x,y),x,y,c,i,j)
   if1#(false(),x,y,c,i,j) -> size#(j)
   if1#(false(),x,y,c,i,j) -> le#(c,size(j))
   if1#(false(),x,y,c,i,j) -> if2#(le(c,size(j)),x,y,c,i,j)
   if2#(true(),x,y,c,edge(u,v,i),j) -> reach#(v,y,s(c),j,j)
   if2#(true(),x,y,c,edge(u,v,i),j) -> eq#(x,u)
   if2#(true(),x,y,c,edge(u,v,i),j) -> and#(eq(x,u),reach(v,y,s(c),j,j))
   if2#(true(),x,y,c,edge(u,v,i),j) -> if2#(true(),x,y,c,i,j)
   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)))
  TRS:
   eq(0(),0()) -> true()
   eq(0(),s(x)) -> false()
   eq(s(x),0()) -> false()
   eq(s(x),s(y)) -> eq(x,y)
   or(true(),y) -> true()
   or(false(),y) -> y
   and(true(),y) -> y
   and(false(),y) -> false()
   size(empty()) -> 0()
   size(edge(x,y,i)) -> s(size(i))
   le(0(),y) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   reachable(x,y,i) -> reach(x,y,0(),i,i)
   reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
   if1(true(),x,y,c,i,j) -> true()
   if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
   if2(false(),x,y,c,i,j) -> false()
   if2(true(),x,y,c,empty(),j) -> false()
   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)))
  Usable Rule Processor:
   DPs:
    eq#(s(x),s(y)) -> eq#(x,y)
    size#(edge(x,y,i)) -> size#(i)
    le#(s(x),s(y)) -> le#(x,y)
    reachable#(x,y,i) -> reach#(x,y,0(),i,i)
    reach#(x,y,c,i,j) -> eq#(x,y)
    reach#(x,y,c,i,j) -> if1#(eq(x,y),x,y,c,i,j)
    if1#(false(),x,y,c,i,j) -> size#(j)
    if1#(false(),x,y,c,i,j) -> le#(c,size(j))
    if1#(false(),x,y,c,i,j) -> if2#(le(c,size(j)),x,y,c,i,j)
    if2#(true(),x,y,c,edge(u,v,i),j) -> reach#(v,y,s(c),j,j)
    if2#(true(),x,y,c,edge(u,v,i),j) -> eq#(x,u)
    if2#(true(),x,y,c,edge(u,v,i),j) -> and#(eq(x,u),reach(v,y,s(c),j,j))
    if2#(true(),x,y,c,edge(u,v,i),j) -> if2#(true(),x,y,c,i,j)
    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)))
   TRS:
    f24(x,y) -> x
    f24(x,y) -> y
    eq(0(),0()) -> true()
    eq(0(),s(x)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    size(empty()) -> 0()
    size(edge(x,y,i)) -> s(size(i))
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
    if1(true(),x,y,c,i,j) -> true()
    if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
    if2(false(),x,y,c,i,j) -> false()
    if2(true(),x,y,c,empty(),j) -> false()
    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)))
    or(true(),y) -> true()
    or(false(),y) -> y
    and(true(),y) -> y
    and(false(),y) -> false()
   CDG Processor:
    DPs:
     eq#(s(x),s(y)) -> eq#(x,y)
     size#(edge(x,y,i)) -> size#(i)
     le#(s(x),s(y)) -> le#(x,y)
     reachable#(x,y,i) -> reach#(x,y,0(),i,i)
     reach#(x,y,c,i,j) -> eq#(x,y)
     reach#(x,y,c,i,j) -> if1#(eq(x,y),x,y,c,i,j)
     if1#(false(),x,y,c,i,j) -> size#(j)
     if1#(false(),x,y,c,i,j) -> le#(c,size(j))
     if1#(false(),x,y,c,i,j) -> if2#(le(c,size(j)),x,y,c,i,j)
     if2#(true(),x,y,c,edge(u,v,i),j) -> reach#(v,y,s(c),j,j)
     if2#(true(),x,y,c,edge(u,v,i),j) -> eq#(x,u)
     if2#(true(),x,y,c,edge(u,v,i),j) -> and#(eq(x,u),reach(v,y,s(c),j,j))
     if2#(true(),x,y,c,edge(u,v,i),j) -> if2#(true(),x,y,c,i,j)
     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)))
    TRS:
     f24(x,y) -> x
     f24(x,y) -> y
     eq(0(),0()) -> true()
     eq(0(),s(x)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     size(empty()) -> 0()
     size(edge(x,y,i)) -> s(size(i))
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
     if1(true(),x,y,c,i,j) -> true()
     if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
     if2(false(),x,y,c,i,j) -> false()
     if2(true(),x,y,c,empty(),j) -> false()
     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)))
     or(true(),y) -> true()
     or(false(),y) -> y
     and(true(),y) -> y
     and(false(),y) -> false()
    graph:
     if2#(true(),x,y,c,edge(u,v,i),j) -> if2#(true(),x,y,c,i,j) ->
     if2#(true(),x,y,c,edge(u,v,i),j) -> reach#(v,y,s(c),j,j)
     if2#(true(),x,y,c,edge(u,v,i),j) -> if2#(true(),x,y,c,i,j) ->
     if2#(true(),x,y,c,edge(u,v,i),j) -> eq#(x,u)
     if2#(true(),x,y,c,edge(u,v,i),j) -> if2#(true(),x,y,c,i,j) ->
     if2#(true(),x,y,c,edge(u,v,i),j) -> and#(eq(x,u),reach(v,y,s(c),j,j))
     if2#(true(),x,y,c,edge(u,v,i),j) -> if2#(true(),x,y,c,i,j) ->
     if2#(true(),x,y,c,edge(u,v,i),j) -> if2#(true(),x,y,c,i,j)
     if2#(true(),x,y,c,edge(u,v,i),j) -> if2#(true(),x,y,c,i,j) ->
     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)))
     if2#(true(),x,y,c,edge(u,v,i),j) -> reach#(v,y,s(c),j,j) ->
     reach#(x,y,c,i,j) -> eq#(x,y)
     if2#(true(),x,y,c,edge(u,v,i),j) -> reach#(v,y,s(c),j,j) ->
     reach#(x,y,c,i,j) -> if1#(eq(x,y),x,y,c,i,j)
     if2#(true(),x,y,c,edge(u,v,i),j) -> eq#(x,u) ->
     eq#(s(x),s(y)) -> eq#(x,y)
     if1#(false(),x,y,c,i,j) -> if2#(le(c,size(j)),x,y,c,i,j) ->
     if2#(true(),x,y,c,edge(u,v,i),j) -> reach#(v,y,s(c),j,j)
     if1#(false(),x,y,c,i,j) -> if2#(le(c,size(j)),x,y,c,i,j) ->
     if2#(true(),x,y,c,edge(u,v,i),j) -> eq#(x,u)
     if1#(false(),x,y,c,i,j) -> if2#(le(c,size(j)),x,y,c,i,j) ->
     if2#(true(),x,y,c,edge(u,v,i),j) -> and#(eq(x,u),reach(v,y,s(c),j,j))
     if1#(false(),x,y,c,i,j) -> if2#(le(c,size(j)),x,y,c,i,j) ->
     if2#(true(),x,y,c,edge(u,v,i),j) -> if2#(true(),x,y,c,i,j)
     if1#(false(),x,y,c,i,j) -> if2#(le(c,size(j)),x,y,c,i,j) ->
     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)))
     if1#(false(),x,y,c,i,j) -> le#(c,size(j)) ->
     le#(s(x),s(y)) -> le#(x,y)
     if1#(false(),x,y,c,i,j) -> size#(j) ->
     size#(edge(x,y,i)) -> size#(i)
     reach#(x,y,c,i,j) -> if1#(eq(x,y),x,y,c,i,j) ->
     if1#(false(),x,y,c,i,j) -> size#(j)
     reach#(x,y,c,i,j) -> if1#(eq(x,y),x,y,c,i,j) ->
     if1#(false(),x,y,c,i,j) -> le#(c,size(j))
     reach#(x,y,c,i,j) -> if1#(eq(x,y),x,y,c,i,j) ->
     if1#(false(),x,y,c,i,j) -> if2#(le(c,size(j)),x,y,c,i,j)
     reach#(x,y,c,i,j) -> eq#(x,y) ->
     eq#(s(x),s(y)) -> eq#(x,y)
     reachable#(x,y,i) -> reach#(x,y,0(),i,i) ->
     reach#(x,y,c,i,j) -> eq#(x,y)
     reachable#(x,y,i) -> reach#(x,y,0(),i,i) ->
     reach#(x,y,c,i,j) -> if1#(eq(x,y),x,y,c,i,j)
     le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
     size#(edge(x,y,i)) -> size#(i) -> size#(edge(x,y,i)) -> size#(i)
     eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y)
    Restore Modifier:
     DPs:
      eq#(s(x),s(y)) -> eq#(x,y)
      size#(edge(x,y,i)) -> size#(i)
      le#(s(x),s(y)) -> le#(x,y)
      reachable#(x,y,i) -> reach#(x,y,0(),i,i)
      reach#(x,y,c,i,j) -> eq#(x,y)
      reach#(x,y,c,i,j) -> if1#(eq(x,y),x,y,c,i,j)
      if1#(false(),x,y,c,i,j) -> size#(j)
      if1#(false(),x,y,c,i,j) -> le#(c,size(j))
      if1#(false(),x,y,c,i,j) -> if2#(le(c,size(j)),x,y,c,i,j)
      if2#(true(),x,y,c,edge(u,v,i),j) -> reach#(v,y,s(c),j,j)
      if2#(true(),x,y,c,edge(u,v,i),j) -> eq#(x,u)
      if2#(true(),x,y,c,edge(u,v,i),j) -> and#(eq(x,u),reach(v,y,s(c),j,j))
      if2#(true(),x,y,c,edge(u,v,i),j) -> if2#(true(),x,y,c,i,j)
      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)))
     TRS:
      eq(0(),0()) -> true()
      eq(0(),s(x)) -> false()
      eq(s(x),0()) -> false()
      eq(s(x),s(y)) -> eq(x,y)
      or(true(),y) -> true()
      or(false(),y) -> y
      and(true(),y) -> y
      and(false(),y) -> false()
      size(empty()) -> 0()
      size(edge(x,y,i)) -> s(size(i))
      le(0(),y) -> true()
      le(s(x),0()) -> false()
      le(s(x),s(y)) -> le(x,y)
      reachable(x,y,i) -> reach(x,y,0(),i,i)
      reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
      if1(true(),x,y,c,i,j) -> true()
      if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
      if2(false(),x,y,c,i,j) -> false()
      if2(true(),x,y,c,empty(),j) -> false()
      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)))
     SCC Processor:
      #sccs: 4
      #rules: 7
      #arcs: 24/196
      DPs:
       if2#(true(),x,y,c,edge(u,v,i),j) -> if2#(true(),x,y,c,i,j)
       if2#(true(),x,y,c,edge(u,v,i),j) -> reach#(v,y,s(c),j,j)
       reach#(x,y,c,i,j) -> if1#(eq(x,y),x,y,c,i,j)
       if1#(false(),x,y,c,i,j) -> if2#(le(c,size(j)),x,y,c,i,j)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(x)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       or(true(),y) -> true()
       or(false(),y) -> y
       and(true(),y) -> y
       and(false(),y) -> false()
       size(empty()) -> 0()
       size(edge(x,y,i)) -> s(size(i))
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       reachable(x,y,i) -> reach(x,y,0(),i,i)
       reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
       if1(true(),x,y,c,i,j) -> true()
       if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
       if2(false(),x,y,c,i,j) -> false()
       if2(true(),x,y,c,empty(),j) -> false()
       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)))
      Open
      
      DPs:
       size#(edge(x,y,i)) -> size#(i)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(x)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       or(true(),y) -> true()
       or(false(),y) -> y
       and(true(),y) -> y
       and(false(),y) -> false()
       size(empty()) -> 0()
       size(edge(x,y,i)) -> s(size(i))
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       reachable(x,y,i) -> reach(x,y,0(),i,i)
       reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
       if1(true(),x,y,c,i,j) -> true()
       if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
       if2(false(),x,y,c,i,j) -> false()
       if2(true(),x,y,c,empty(),j) -> false()
       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)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [size#](x0) = x0 + 1,
        
        [if2](x0, x1, x2, x3, x4, x5) = 0,
        
        [if1](x0, x1, x2, x3, x4, x5) = 0,
        
        [reach](x0, x1, x2, x3, x4) = 0,
        
        [reachable](x0, x1, x2) = 0,
        
        [le](x0, x1) = 0,
        
        [edge](x0, x1, x2) = x2 + 1,
        
        [size](x0) = 0,
        
        [empty] = 0,
        
        [and](x0, x1) = x1,
        
        [or](x0, x1) = x1,
        
        [false] = 0,
        
        [s](x0) = 0,
        
        [true] = 0,
        
        [eq](x0, x1) = 0,
        
        [0] = 0
       orientation:
        size#(edge(x,y,i)) = i + 2 >= i + 1 = size#(i)
        
        eq(0(),0()) = 0 >= 0 = true()
        
        eq(0(),s(x)) = 0 >= 0 = false()
        
        eq(s(x),0()) = 0 >= 0 = false()
        
        eq(s(x),s(y)) = 0 >= 0 = eq(x,y)
        
        or(true(),y) = y >= 0 = true()
        
        or(false(),y) = y >= y = y
        
        and(true(),y) = y >= y = y
        
        and(false(),y) = y >= 0 = false()
        
        size(empty()) = 0 >= 0 = 0()
        
        size(edge(x,y,i)) = 0 >= 0 = s(size(i))
        
        le(0(),y) = 0 >= 0 = true()
        
        le(s(x),0()) = 0 >= 0 = false()
        
        le(s(x),s(y)) = 0 >= 0 = le(x,y)
        
        reachable(x,y,i) = 0 >= 0 = reach(x,y,0(),i,i)
        
        reach(x,y,c,i,j) = 0 >= 0 = if1(eq(x,y),x,y,c,i,j)
        
        if1(true(),x,y,c,i,j) = 0 >= 0 = true()
        
        if1(false(),x,y,c,i,j) = 0 >= 0 = if2(le(c,size(j)),x,y,c,i,j)
        
        if2(false(),x,y,c,i,j) = 0 >= 0 = false()
        
        if2(true(),x,y,c,empty(),j) = 0 >= 0 = false()
        
        if2(true(),x,y,c,edge(u,v,i),j) = 0 >= 0 = or(if2(true(),x,y,c,i,j),and(eq(x,u),reach(v,y,s(c),j,j)))
       problem:
        DPs:
         
        TRS:
         eq(0(),0()) -> true()
         eq(0(),s(x)) -> false()
         eq(s(x),0()) -> false()
         eq(s(x),s(y)) -> eq(x,y)
         or(true(),y) -> true()
         or(false(),y) -> y
         and(true(),y) -> y
         and(false(),y) -> false()
         size(empty()) -> 0()
         size(edge(x,y,i)) -> s(size(i))
         le(0(),y) -> true()
         le(s(x),0()) -> false()
         le(s(x),s(y)) -> le(x,y)
         reachable(x,y,i) -> reach(x,y,0(),i,i)
         reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
         if1(true(),x,y,c,i,j) -> true()
         if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
         if2(false(),x,y,c,i,j) -> false()
         if2(true(),x,y,c,empty(),j) -> false()
         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)))
       Qed
      
      DPs:
       le#(s(x),s(y)) -> le#(x,y)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(x)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       or(true(),y) -> true()
       or(false(),y) -> y
       and(true(),y) -> y
       and(false(),y) -> false()
       size(empty()) -> 0()
       size(edge(x,y,i)) -> s(size(i))
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       reachable(x,y,i) -> reach(x,y,0(),i,i)
       reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
       if1(true(),x,y,c,i,j) -> true()
       if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
       if2(false(),x,y,c,i,j) -> false()
       if2(true(),x,y,c,empty(),j) -> false()
       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)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [le#](x0, x1) = x1 + 1,
        
        [if2](x0, x1, x2, x3, x4, x5) = 0,
        
        [if1](x0, x1, x2, x3, x4, x5) = 0,
        
        [reach](x0, x1, x2, x3, x4) = 0,
        
        [reachable](x0, x1, x2) = 0,
        
        [le](x0, x1) = 0,
        
        [edge](x0, x1, x2) = x2 + 1,
        
        [size](x0) = x0 + 1,
        
        [empty] = 0,
        
        [and](x0, x1) = x1,
        
        [or](x0, x1) = x1,
        
        [false] = 0,
        
        [s](x0) = x0 + 1,
        
        [true] = 0,
        
        [eq](x0, x1) = 0,
        
        [0] = 1
       orientation:
        le#(s(x),s(y)) = y + 2 >= y + 1 = le#(x,y)
        
        eq(0(),0()) = 0 >= 0 = true()
        
        eq(0(),s(x)) = 0 >= 0 = false()
        
        eq(s(x),0()) = 0 >= 0 = false()
        
        eq(s(x),s(y)) = 0 >= 0 = eq(x,y)
        
        or(true(),y) = y >= 0 = true()
        
        or(false(),y) = y >= y = y
        
        and(true(),y) = y >= y = y
        
        and(false(),y) = y >= 0 = false()
        
        size(empty()) = 1 >= 1 = 0()
        
        size(edge(x,y,i)) = i + 2 >= i + 2 = s(size(i))
        
        le(0(),y) = 0 >= 0 = true()
        
        le(s(x),0()) = 0 >= 0 = false()
        
        le(s(x),s(y)) = 0 >= 0 = le(x,y)
        
        reachable(x,y,i) = 0 >= 0 = reach(x,y,0(),i,i)
        
        reach(x,y,c,i,j) = 0 >= 0 = if1(eq(x,y),x,y,c,i,j)
        
        if1(true(),x,y,c,i,j) = 0 >= 0 = true()
        
        if1(false(),x,y,c,i,j) = 0 >= 0 = if2(le(c,size(j)),x,y,c,i,j)
        
        if2(false(),x,y,c,i,j) = 0 >= 0 = false()
        
        if2(true(),x,y,c,empty(),j) = 0 >= 0 = false()
        
        if2(true(),x,y,c,edge(u,v,i),j) = 0 >= 0 = or(if2(true(),x,y,c,i,j),and(eq(x,u),reach(v,y,s(c),j,j)))
       problem:
        DPs:
         
        TRS:
         eq(0(),0()) -> true()
         eq(0(),s(x)) -> false()
         eq(s(x),0()) -> false()
         eq(s(x),s(y)) -> eq(x,y)
         or(true(),y) -> true()
         or(false(),y) -> y
         and(true(),y) -> y
         and(false(),y) -> false()
         size(empty()) -> 0()
         size(edge(x,y,i)) -> s(size(i))
         le(0(),y) -> true()
         le(s(x),0()) -> false()
         le(s(x),s(y)) -> le(x,y)
         reachable(x,y,i) -> reach(x,y,0(),i,i)
         reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
         if1(true(),x,y,c,i,j) -> true()
         if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
         if2(false(),x,y,c,i,j) -> false()
         if2(true(),x,y,c,empty(),j) -> false()
         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)))
       Qed
      
      DPs:
       eq#(s(x),s(y)) -> eq#(x,y)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(x)) -> false()
       eq(s(x),0()) -> false()
       eq(s(x),s(y)) -> eq(x,y)
       or(true(),y) -> true()
       or(false(),y) -> y
       and(true(),y) -> y
       and(false(),y) -> false()
       size(empty()) -> 0()
       size(edge(x,y,i)) -> s(size(i))
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       reachable(x,y,i) -> reach(x,y,0(),i,i)
       reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
       if1(true(),x,y,c,i,j) -> true()
       if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
       if2(false(),x,y,c,i,j) -> false()
       if2(true(),x,y,c,empty(),j) -> false()
       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)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [eq#](x0, x1) = x1 + 1,
        
        [if2](x0, x1, x2, x3, x4, x5) = 0,
        
        [if1](x0, x1, x2, x3, x4, x5) = 0,
        
        [reach](x0, x1, x2, x3, x4) = 0,
        
        [reachable](x0, x1, x2) = 0,
        
        [le](x0, x1) = 0,
        
        [edge](x0, x1, x2) = x2 + 1,
        
        [size](x0) = x0 + 1,
        
        [empty] = 0,
        
        [and](x0, x1) = x1,
        
        [or](x0, x1) = x1,
        
        [false] = 0,
        
        [s](x0) = x0 + 1,
        
        [true] = 0,
        
        [eq](x0, x1) = 0,
        
        [0] = 1
       orientation:
        eq#(s(x),s(y)) = y + 2 >= y + 1 = eq#(x,y)
        
        eq(0(),0()) = 0 >= 0 = true()
        
        eq(0(),s(x)) = 0 >= 0 = false()
        
        eq(s(x),0()) = 0 >= 0 = false()
        
        eq(s(x),s(y)) = 0 >= 0 = eq(x,y)
        
        or(true(),y) = y >= 0 = true()
        
        or(false(),y) = y >= y = y
        
        and(true(),y) = y >= y = y
        
        and(false(),y) = y >= 0 = false()
        
        size(empty()) = 1 >= 1 = 0()
        
        size(edge(x,y,i)) = i + 2 >= i + 2 = s(size(i))
        
        le(0(),y) = 0 >= 0 = true()
        
        le(s(x),0()) = 0 >= 0 = false()
        
        le(s(x),s(y)) = 0 >= 0 = le(x,y)
        
        reachable(x,y,i) = 0 >= 0 = reach(x,y,0(),i,i)
        
        reach(x,y,c,i,j) = 0 >= 0 = if1(eq(x,y),x,y,c,i,j)
        
        if1(true(),x,y,c,i,j) = 0 >= 0 = true()
        
        if1(false(),x,y,c,i,j) = 0 >= 0 = if2(le(c,size(j)),x,y,c,i,j)
        
        if2(false(),x,y,c,i,j) = 0 >= 0 = false()
        
        if2(true(),x,y,c,empty(),j) = 0 >= 0 = false()
        
        if2(true(),x,y,c,edge(u,v,i),j) = 0 >= 0 = or(if2(true(),x,y,c,i,j),and(eq(x,u),reach(v,y,s(c),j,j)))
       problem:
        DPs:
         
        TRS:
         eq(0(),0()) -> true()
         eq(0(),s(x)) -> false()
         eq(s(x),0()) -> false()
         eq(s(x),s(y)) -> eq(x,y)
         or(true(),y) -> true()
         or(false(),y) -> y
         and(true(),y) -> y
         and(false(),y) -> false()
         size(empty()) -> 0()
         size(edge(x,y,i)) -> s(size(i))
         le(0(),y) -> true()
         le(s(x),0()) -> false()
         le(s(x),s(y)) -> le(x,y)
         reachable(x,y,i) -> reach(x,y,0(),i,i)
         reach(x,y,c,i,j) -> if1(eq(x,y),x,y,c,i,j)
         if1(true(),x,y,c,i,j) -> true()
         if1(false(),x,y,c,i,j) -> if2(le(c,size(j)),x,y,c,i,j)
         if2(false(),x,y,c,i,j) -> false()
         if2(true(),x,y,c,empty(),j) -> false()
         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)))
       Qed