MAYBE
Time: 0.446

Problem:
 Equations:
  unionAC(unionAC(x3,x4),x5) -> unionAC(x3,unionAC(x4,x5))
  unionAC(x3,x4) -> unionAC(x4,x3)
  interAC(interAC(x3,x4),x5) -> interAC(x3,interAC(x4,x5))
  interAC(x3,x4) -> interAC(x4,x3)
  unionAC(x3,unionAC(x4,x5)) -> unionAC(unionAC(x3,x4),x5)
  unionAC(x4,x3) -> unionAC(x3,x4)
  interAC(x3,interAC(x4,x5)) -> interAC(interAC(x3,x4),x5)
  interAC(x4,x3) -> interAC(x3,x4)
 TRS:
  if(true(),x,y) -> x
  if(false(),x,y) -> y
  eqC(0(),0()) -> true()
  eqC(0(),s(x)) -> false()
  eqC(s(x),s(y)) -> eqC(x,y)
  unionAC(empty(),x) -> x
  interAC(empty(),x) -> empty()
  interAC(unionAC(y,z),x) -> unionAC(interAC(x,y),interAC(x,z))
  interAC(singl(x),singl(y)) -> if(eqC(x,y),singl(x),empty())

Proof:
 DP Processor:
  Equations#:
   union{AC,#}(unionAC(x3,x4),x5) -> union{AC,#}(x3,unionAC(x4,x5))
   union{AC,#}(x3,x4) -> union{AC,#}(x4,x3)
   inter{AC,#}(interAC(x3,x4),x5) -> inter{AC,#}(x3,interAC(x4,x5))
   inter{AC,#}(x3,x4) -> inter{AC,#}(x4,x3)
   union{AC,#}(x3,unionAC(x4,x5)) -> union{AC,#}(unionAC(x3,x4),x5)
   union{AC,#}(x4,x3) -> union{AC,#}(x3,x4)
   inter{AC,#}(x3,interAC(x4,x5)) -> inter{AC,#}(interAC(x3,x4),x5)
   inter{AC,#}(x4,x3) -> inter{AC,#}(x3,x4)
  DPs:
   eq{C,#}(s(x),s(y)) -> eq{C,#}(x,y)
   inter{AC,#}(unionAC(y,z),x) -> inter{AC,#}(x,z)
   inter{AC,#}(unionAC(y,z),x) -> inter{AC,#}(x,y)
   inter{AC,#}(unionAC(y,z),x) -> union{AC,#}(interAC(x,y),interAC(x,z))
   inter{AC,#}(singl(x),singl(y)) -> eq{C,#}(x,y)
   inter{AC,#}(singl(x),singl(y)) -> if#(eqC(x,y),singl(x),empty())
   union{AC,#}(x6,unionAC(empty(),x)) -> union{AC,#}(x6,x)
   inter{AC,#}(x7,interAC(empty(),x)) -> inter{AC,#}(x7,empty())
   inter{AC,#}(x8,interAC(unionAC(y,z),x)) -> inter{AC,#}(x,z)
   inter{AC,#}(x8,interAC(unionAC(y,z),x)) -> inter{AC,#}(x,y)
   inter{AC,#}(x8,interAC(unionAC(y,z),x)) -> union{AC,#}(interAC(x,y),interAC(x,z))
   inter{AC,#}(x8,interAC(unionAC(y,z),x)) -> inter{AC,#}(x8,unionAC(interAC(x,y),interAC(x,z)))
   inter{AC,#}(x9,interAC(singl(x),singl(y))) -> eq{C,#}(x,y)
   inter{AC,#}(x9,interAC(singl(x),singl(y))) -> if#(eqC(x,y),singl(x),empty())
   inter{AC,#}(x9,interAC(singl(x),singl(y))) -> inter{AC,#}(x9,if(eqC(x,y),singl(x),empty()))
  Equations:
   unionAC(unionAC(x3,x4),x5) -> unionAC(x3,unionAC(x4,x5))
   unionAC(x3,x4) -> unionAC(x4,x3)
   interAC(interAC(x3,x4),x5) -> interAC(x3,interAC(x4,x5))
   interAC(x3,x4) -> interAC(x4,x3)
   unionAC(x3,unionAC(x4,x5)) -> unionAC(unionAC(x3,x4),x5)
   unionAC(x4,x3) -> unionAC(x3,x4)
   interAC(x3,interAC(x4,x5)) -> interAC(interAC(x3,x4),x5)
   interAC(x4,x3) -> interAC(x3,x4)
  TRS:
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   eqC(0(),0()) -> true()
   eqC(0(),s(x)) -> false()
   eqC(s(x),s(y)) -> eqC(x,y)
   unionAC(empty(),x) -> x
   interAC(empty(),x) -> empty()
   interAC(unionAC(y,z),x) -> unionAC(interAC(x,y),interAC(x,z))
   interAC(singl(x),singl(y)) -> if(eqC(x,y),singl(x),empty())
  S:
   union{AC,#}(unionAC(x10,x11),x12) -> union{AC,#}(x10,x11)
   union{AC,#}(x10,unionAC(x11,x12)) -> union{AC,#}(x11,x12)
   inter{AC,#}(interAC(x10,x11),x12) -> inter{AC,#}(x10,x11)
   inter{AC,#}(x10,interAC(x11,x12)) -> inter{AC,#}(x11,x12)
  AC-EDG Processor:
   Equations#:
    union{AC,#}(unionAC(x3,x4),x5) -> union{AC,#}(x3,unionAC(x4,x5))
    union{AC,#}(x3,x4) -> union{AC,#}(x4,x3)
    inter{AC,#}(interAC(x3,x4),x5) -> inter{AC,#}(x3,interAC(x4,x5))
    inter{AC,#}(x3,x4) -> inter{AC,#}(x4,x3)
    union{AC,#}(x3,unionAC(x4,x5)) -> union{AC,#}(unionAC(x3,x4),x5)
    union{AC,#}(x4,x3) -> union{AC,#}(x3,x4)
    inter{AC,#}(x3,interAC(x4,x5)) -> inter{AC,#}(interAC(x3,x4),x5)
    inter{AC,#}(x4,x3) -> inter{AC,#}(x3,x4)
   DPs:
    eq{C,#}(s(x),s(y)) -> eq{C,#}(x,y)
    inter{AC,#}(unionAC(y,z),x) -> inter{AC,#}(x,z)
    inter{AC,#}(unionAC(y,z),x) -> inter{AC,#}(x,y)
    inter{AC,#}(unionAC(y,z),x) -> union{AC,#}(interAC(x,y),interAC(x,z))
    inter{AC,#}(singl(x),singl(y)) -> eq{C,#}(x,y)
    inter{AC,#}(singl(x),singl(y)) -> if#(eqC(x,y),singl(x),empty())
    union{AC,#}(x6,unionAC(empty(),x)) -> union{AC,#}(x6,x)
    inter{AC,#}(x7,interAC(empty(),x)) -> inter{AC,#}(x7,empty())
    inter{AC,#}(x8,interAC(unionAC(y,z),x)) -> inter{AC,#}(x,z)
    inter{AC,#}(x8,interAC(unionAC(y,z),x)) -> inter{AC,#}(x,y)
    inter{AC,#}(x8,interAC(unionAC(y,z),x)) -> union{AC,#}(interAC(x,y),interAC(x,z))
    inter{AC,#}(x8,interAC(unionAC(y,z),x)) -> inter{AC,#}(x8,unionAC(interAC(x,y),interAC(x,z)))
    inter{AC,#}(x9,interAC(singl(x),singl(y))) -> eq{C,#}(x,y)
    inter{AC,#}(x9,interAC(singl(x),singl(y))) -> if#(eqC(x,y),singl(x),empty())
    inter{AC,#}(x9,interAC(singl(x),singl(y))) -> inter{AC,#}(x9,if(eqC(x,y),singl(x),empty()))
   Equations:
    unionAC(unionAC(x3,x4),x5) -> unionAC(x3,unionAC(x4,x5))
    unionAC(x3,x4) -> unionAC(x4,x3)
    interAC(interAC(x3,x4),x5) -> interAC(x3,interAC(x4,x5))
    interAC(x3,x4) -> interAC(x4,x3)
    unionAC(x3,unionAC(x4,x5)) -> unionAC(unionAC(x3,x4),x5)
    unionAC(x4,x3) -> unionAC(x3,x4)
    interAC(x3,interAC(x4,x5)) -> interAC(interAC(x3,x4),x5)
    interAC(x4,x3) -> interAC(x3,x4)
   TRS:
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    eqC(0(),0()) -> true()
    eqC(0(),s(x)) -> false()
    eqC(s(x),s(y)) -> eqC(x,y)
    unionAC(empty(),x) -> x
    interAC(empty(),x) -> empty()
    interAC(unionAC(y,z),x) -> unionAC(interAC(x,y),interAC(x,z))
    interAC(singl(x),singl(y)) -> if(eqC(x,y),singl(x),empty())
   S:
    union{AC,#}(unionAC(x10,x11),x12) -> union{AC,#}(x10,x11)
    union{AC,#}(x10,unionAC(x11,x12)) -> union{AC,#}(x11,x12)
    inter{AC,#}(interAC(x10,x11),x12) -> inter{AC,#}(x10,x11)
    inter{AC,#}(x10,interAC(x11,x12)) -> inter{AC,#}(x11,x12)
   Open