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)))
  TDG 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)))
   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) -> 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) -> 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) -> 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) -> 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) -> 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) -> if1#(eq(x,y),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) -> eq#(x,y)
    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) -> 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) -> 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) -> 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) -> 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) -> 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) -> if2#(le(c,size(j)),x,y,c,i,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) -> size#(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) -> if1#(eq(x,y),x,y,c,i,j)
    reachable#(x,y,i) -> reach#(x,y,0(),i,i) ->
    reach#(x,y,c,i,j) -> eq#(x,y)
    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)
   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:
     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)))
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 1
     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:
     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)))
    Subterm Criterion Processor:
     simple projection:
      pi(size#) = 0
     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)))
    Subterm Criterion Processor:
     simple projection:
      pi(eq#) = 1
     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