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
 union(empty(),h) -> h
 union(edge(x,y,i),h) -> edge(x,y,union(i,h))
 reach(x,y,empty(),h) -> false()
 reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
 if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h)
 if_reach_2(true(),x,y,edge(u,v,i),h) -> true()
 if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
 if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h))

Proof:
 DP Processor:
  DPs:
   eq#(s(x),s(y)) -> eq#(x,y)
   union#(edge(x,y,i),h) -> union#(i,h)
   reach#(x,y,edge(u,v,i),h) -> eq#(x,u)
   reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h)
   if_reach_1#(true(),x,y,edge(u,v,i),h) -> eq#(y,v)
   if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eq(y,v),x,y,edge(u,v,i),h)
   if_reach_2#(false(),x,y,edge(u,v,i),h) -> union#(i,h)
   if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty())
   if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h)
   if_reach_2#(false(),x,y,edge(u,v,i),h) -> or#(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
   if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h))
  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
   union(empty(),h) -> h
   union(edge(x,y,i),h) -> edge(x,y,union(i,h))
   reach(x,y,empty(),h) -> false()
   reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
   if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h)
   if_reach_2(true(),x,y,edge(u,v,i),h) -> true()
   if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
   if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h))
  TDG Processor:
   DPs:
    eq#(s(x),s(y)) -> eq#(x,y)
    union#(edge(x,y,i),h) -> union#(i,h)
    reach#(x,y,edge(u,v,i),h) -> eq#(x,u)
    reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h)
    if_reach_1#(true(),x,y,edge(u,v,i),h) -> eq#(y,v)
    if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eq(y,v),x,y,edge(u,v,i),h)
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> union#(i,h)
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty())
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h)
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> or#(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
    if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h))
   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
    union(empty(),h) -> h
    union(edge(x,y,i),h) -> edge(x,y,union(i,h))
    reach(x,y,empty(),h) -> false()
    reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
    if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h)
    if_reach_2(true(),x,y,edge(u,v,i),h) -> true()
    if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
    if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h))
   graph:
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty()) ->
    reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h)
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty()) ->
    reach#(x,y,edge(u,v,i),h) -> eq#(x,u)
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h) ->
    reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h)
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h) ->
    reach#(x,y,edge(u,v,i),h) -> eq#(x,u)
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> union#(i,h) ->
    union#(edge(x,y,i),h) -> union#(i,h)
    if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h)) ->
    reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h)
    if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h)) ->
    reach#(x,y,edge(u,v,i),h) -> eq#(x,u)
    if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eq(y,v),x,y,edge(u,v,i),h) ->
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> or#(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
    if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eq(y,v),x,y,edge(u,v,i),h) ->
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h)
    if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eq(y,v),x,y,edge(u,v,i),h) ->
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty())
    if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eq(y,v),x,y,edge(u,v,i),h) ->
    if_reach_2#(false(),x,y,edge(u,v,i),h) -> union#(i,h)
    if_reach_1#(true(),x,y,edge(u,v,i),h) -> eq#(y,v) ->
    eq#(s(x),s(y)) -> eq#(x,y)
    reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) ->
    if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h))
    reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) ->
    if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eq(y,v),x,y,edge(u,v,i),h)
    reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) ->
    if_reach_1#(true(),x,y,edge(u,v,i),h) -> eq#(y,v)
    reach#(x,y,edge(u,v,i),h) -> eq#(x,u) ->
    eq#(s(x),s(y)) -> eq#(x,y)
    union#(edge(x,y,i),h) -> union#(i,h) ->
    union#(edge(x,y,i),h) -> union#(i,h)
    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)
     union#(edge(x,y,i),h) -> union#(i,h)
     reach#(x,y,edge(u,v,i),h) -> eq#(x,u)
     reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h)
     if_reach_1#(true(),x,y,edge(u,v,i),h) -> eq#(y,v)
     if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eq(y,v),x,y,edge(u,v,i),h)
     if_reach_2#(false(),x,y,edge(u,v,i),h) -> union#(i,h)
     if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty())
     if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h)
     if_reach_2#(false(),x,y,edge(u,v,i),h) -> or#(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
     if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h))
    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
     union(empty(),h) -> h
     union(edge(x,y,i),h) -> edge(x,y,union(i,h))
     reach(x,y,empty(),h) -> false()
     reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
     if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h)
     if_reach_2(true(),x,y,edge(u,v,i),h) -> true()
     if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
     if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h))
    SCC Processor:
     #sccs: 3
     #rules: 7
     #arcs: 18/121
     DPs:
      if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty())
      reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h)
      if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eq(y,v),x,y,edge(u,v,i),h)
      if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h)
      if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h))
     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
      union(empty(),h) -> h
      union(edge(x,y,i),h) -> edge(x,y,union(i,h))
      reach(x,y,empty(),h) -> false()
      reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
      if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h)
      if_reach_2(true(),x,y,edge(u,v,i),h) -> true()
      if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
      if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h))
     Open
     
     DPs:
      union#(edge(x,y,i),h) -> union#(i,h)
     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
      union(empty(),h) -> h
      union(edge(x,y,i),h) -> edge(x,y,union(i,h))
      reach(x,y,empty(),h) -> false()
      reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
      if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h)
      if_reach_2(true(),x,y,edge(u,v,i),h) -> true()
      if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
      if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h))
     Open
     
     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
      union(empty(),h) -> h
      union(edge(x,y,i),h) -> edge(x,y,union(i,h))
      reach(x,y,empty(),h) -> false()
      reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
      if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h)
      if_reach_2(true(),x,y,edge(u,v,i),h) -> true()
      if_reach_2(false(),x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
      if_reach_1(false(),x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h))
     Open