MAYBE
Time: 0.420

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
  eq(0(),0()) -> true()
  eq(0(),s(x)) -> false()
  eq(s(x),s(y)) -> eq(x,y)
  unionAC(empty(),x) -> x
  interAC(x,empty()) -> empty()
  interAC(x,unionAC(y,z)) -> unionAC(interAC(x,y),interAC(x,z))
  interAC(single(x),single(y)) -> if(eq(x,y),single(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#(s(x),s(y)) -> eq#(x,y)
   inter{AC,#}(x,unionAC(y,z)) -> inter{AC,#}(x,z)
   inter{AC,#}(x,unionAC(y,z)) -> inter{AC,#}(x,y)
   inter{AC,#}(x,unionAC(y,z)) -> union{AC,#}(interAC(x,y),interAC(x,z))
   inter{AC,#}(single(x),single(y)) -> eq#(x,y)
   inter{AC,#}(single(x),single(y)) -> if#(eq(x,y),single(x),empty())
   union{AC,#}(x6,unionAC(empty(),x)) -> union{AC,#}(x6,x)
   inter{AC,#}(x7,interAC(x,empty())) -> inter{AC,#}(x7,empty())
   inter{AC,#}(x8,interAC(x,unionAC(y,z))) -> inter{AC,#}(x,z)
   inter{AC,#}(x8,interAC(x,unionAC(y,z))) -> inter{AC,#}(x,y)
   inter{AC,#}(x8,interAC(x,unionAC(y,z))) -> union{AC,#}(interAC(x,y),interAC(x,z))
   inter{AC,#}(x8,interAC(x,unionAC(y,z))) -> inter{AC,#}(x8,unionAC(interAC(x,y),interAC(x,z)))
   inter{AC,#}(x9,interAC(single(x),single(y))) -> eq#(x,y)
   inter{AC,#}(x9,interAC(single(x),single(y))) -> if#(eq(x,y),single(x),empty())
   inter{AC,#}(x9,interAC(single(x),single(y))) -> inter{AC,#}(x9,if(eq(x,y),single(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
   eq(0(),0()) -> true()
   eq(0(),s(x)) -> false()
   eq(s(x),s(y)) -> eq(x,y)
   unionAC(empty(),x) -> x
   interAC(x,empty()) -> empty()
   interAC(x,unionAC(y,z)) -> unionAC(interAC(x,y),interAC(x,z))
   interAC(single(x),single(y)) -> if(eq(x,y),single(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#(s(x),s(y)) -> eq#(x,y)
    inter{AC,#}(x,unionAC(y,z)) -> inter{AC,#}(x,z)
    inter{AC,#}(x,unionAC(y,z)) -> inter{AC,#}(x,y)
    inter{AC,#}(x,unionAC(y,z)) -> union{AC,#}(interAC(x,y),interAC(x,z))
    inter{AC,#}(single(x),single(y)) -> eq#(x,y)
    inter{AC,#}(single(x),single(y)) -> if#(eq(x,y),single(x),empty())
    union{AC,#}(x6,unionAC(empty(),x)) -> union{AC,#}(x6,x)
    inter{AC,#}(x7,interAC(x,empty())) -> inter{AC,#}(x7,empty())
    inter{AC,#}(x8,interAC(x,unionAC(y,z))) -> inter{AC,#}(x,z)
    inter{AC,#}(x8,interAC(x,unionAC(y,z))) -> inter{AC,#}(x,y)
    inter{AC,#}(x8,interAC(x,unionAC(y,z))) -> union{AC,#}(interAC(x,y),interAC(x,z))
    inter{AC,#}(x8,interAC(x,unionAC(y,z))) -> inter{AC,#}(x8,unionAC(interAC(x,y),interAC(x,z)))
    inter{AC,#}(x9,interAC(single(x),single(y))) -> eq#(x,y)
    inter{AC,#}(x9,interAC(single(x),single(y))) -> if#(eq(x,y),single(x),empty())
    inter{AC,#}(x9,interAC(single(x),single(y))) -> inter{AC,#}(x9,if(eq(x,y),single(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
    eq(0(),0()) -> true()
    eq(0(),s(x)) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    unionAC(empty(),x) -> x
    interAC(x,empty()) -> empty()
    interAC(x,unionAC(y,z)) -> unionAC(interAC(x,y),interAC(x,z))
    interAC(single(x),single(y)) -> if(eq(x,y),single(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