MAYBE
Time: 1.869

Problem:
 Equations:
  orAC(orAC(x6,x7),x8) -> orAC(x6,orAC(x7,x8))
  orAC(x6,x7) -> orAC(x7,x6)
  orAC(x6,orAC(x7,x8)) -> orAC(orAC(x6,x7),x8)
  orAC(x7,x6) -> orAC(x6,x7)
 TRS:
  eqC(0(),0()) -> true()
  eqC(0(),s(x)) -> false()
  eqC(s(x),0()) -> false()
  eqC(s(x),s(y)) -> eqC(x,y)
  orAC(true(),y) -> true()
  orAC(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(eqC(x,u),x,y,edge(u,v,i),h)
  if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eqC(y,v),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))
  if_reach_2(true(),x,y,edge(u,v,i),h) -> true()
  if_reach_2(false(),x,y,edge(u,v,i),h) -> orAC(reach(x,y,i,h),reach(v,y,union(i,h),empty()))

Proof:
 DP Processor:
  Equations#:
   or{AC,#}(orAC(x6,x7),x8) -> or{AC,#}(x6,orAC(x7,x8))
   or{AC,#}(x6,x7) -> or{AC,#}(x7,x6)
   or{AC,#}(x6,orAC(x7,x8)) -> or{AC,#}(orAC(x6,x7),x8)
   or{AC,#}(x7,x6) -> or{AC,#}(x6,x7)
  DPs:
   eq{C,#}(s(x),s(y)) -> eq{C,#}(x,y)
   union#(edge(x,y,i),h) -> union#(i,h)
   reach#(x,y,edge(u,v,i),h) -> eq{C,#}(x,u)
   reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eqC(x,u),x,y,edge(u,v,i),h)
   if_reach_1#(true(),x,y,edge(u,v,i),h) -> eq{C,#}(y,v)
   if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eqC(y,v),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))
   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{AC,#}(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
   or{AC,#}(x9,orAC(true(),y)) -> or{AC,#}(x9,true())
   or{AC,#}(x10,orAC(false(),y)) -> or{AC,#}(x10,y)
  Equations:
   orAC(orAC(x6,x7),x8) -> orAC(x6,orAC(x7,x8))
   orAC(x6,x7) -> orAC(x7,x6)
   orAC(x6,orAC(x7,x8)) -> orAC(orAC(x6,x7),x8)
   orAC(x7,x6) -> orAC(x6,x7)
  TRS:
   eqC(0(),0()) -> true()
   eqC(0(),s(x)) -> false()
   eqC(s(x),0()) -> false()
   eqC(s(x),s(y)) -> eqC(x,y)
   orAC(true(),y) -> true()
   orAC(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(eqC(x,u),x,y,edge(u,v,i),h)
   if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eqC(y,v),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))
   if_reach_2(true(),x,y,edge(u,v,i),h) -> true()
   if_reach_2(false(),x,y,edge(u,v,i),h) -> orAC(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
  S:
   or{AC,#}(orAC(x11,x12),x13) -> or{AC,#}(x11,x12)
   or{AC,#}(x11,orAC(x12,x13)) -> or{AC,#}(x12,x13)
  AC-EDG Processor:
   Equations#:
    or{AC,#}(orAC(x6,x7),x8) -> or{AC,#}(x6,orAC(x7,x8))
    or{AC,#}(x6,x7) -> or{AC,#}(x7,x6)
    or{AC,#}(x6,orAC(x7,x8)) -> or{AC,#}(orAC(x6,x7),x8)
    or{AC,#}(x7,x6) -> or{AC,#}(x6,x7)
   DPs:
    eq{C,#}(s(x),s(y)) -> eq{C,#}(x,y)
    union#(edge(x,y,i),h) -> union#(i,h)
    reach#(x,y,edge(u,v,i),h) -> eq{C,#}(x,u)
    reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eqC(x,u),x,y,edge(u,v,i),h)
    if_reach_1#(true(),x,y,edge(u,v,i),h) -> eq{C,#}(y,v)
    if_reach_1#(true(),x,y,edge(u,v,i),h) -> if_reach_2#(eqC(y,v),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))
    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{AC,#}(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
    or{AC,#}(x9,orAC(true(),y)) -> or{AC,#}(x9,true())
    or{AC,#}(x10,orAC(false(),y)) -> or{AC,#}(x10,y)
   Equations:
    orAC(orAC(x6,x7),x8) -> orAC(x6,orAC(x7,x8))
    orAC(x6,x7) -> orAC(x7,x6)
    orAC(x6,orAC(x7,x8)) -> orAC(orAC(x6,x7),x8)
    orAC(x7,x6) -> orAC(x6,x7)
   TRS:
    eqC(0(),0()) -> true()
    eqC(0(),s(x)) -> false()
    eqC(s(x),0()) -> false()
    eqC(s(x),s(y)) -> eqC(x,y)
    orAC(true(),y) -> true()
    orAC(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(eqC(x,u),x,y,edge(u,v,i),h)
    if_reach_1(true(),x,y,edge(u,v,i),h) -> if_reach_2(eqC(y,v),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))
    if_reach_2(true(),x,y,edge(u,v,i),h) -> true()
    if_reach_2(false(),x,y,edge(u,v,i),h) -> orAC(reach(x,y,i,h),reach(v,y,union(i,h),empty()))
   S:
    or{AC,#}(orAC(x11,x12),x13) -> or{AC,#}(x11,x12)
    or{AC,#}(x11,orAC(x12,x13)) -> or{AC,#}(x12,x13)
   Open