MAYBE
Time: 0.517

Problem:
 Equations:
  eqAC(eqAC(x3,x4),x5) -> eqAC(x3,eqAC(x4,x5))
  eqAC(x3,x4) -> eqAC(x4,x3)
  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)
  eqAC(x3,eqAC(x4,x5)) -> eqAC(eqAC(x3,x4),x5)
  eqAC(x4,x3) -> eqAC(x3,x4)
  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
  eqAC(0(),0()) -> true()
  eqAC(0(),1()) -> false()
  eqAC(1(),1()) -> true()
  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(eqAC(x,y),single(x),empty())

Proof:
 DP Processor:
  Equations#:
   eq{AC,#}(eqAC(x3,x4),x5) -> eq{AC,#}(x3,eqAC(x4,x5))
   eq{AC,#}(x3,x4) -> eq{AC,#}(x4,x3)
   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)
   eq{AC,#}(x3,eqAC(x4,x5)) -> eq{AC,#}(eqAC(x3,x4),x5)
   eq{AC,#}(x4,x3) -> eq{AC,#}(x3,x4)
   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:
   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{AC,#}(x,y)
   inter{AC,#}(single(x),single(y)) -> if#(eqAC(x,y),single(x),empty())
   eq{AC,#}(x6,eqAC(0(),0())) -> eq{AC,#}(x6,true())
   eq{AC,#}(x7,eqAC(0(),1())) -> eq{AC,#}(x7,false())
   eq{AC,#}(x8,eqAC(1(),1())) -> eq{AC,#}(x8,true())
   union{AC,#}(x9,unionAC(empty(),x)) -> union{AC,#}(x9,x)
   inter{AC,#}(x10,interAC(x,empty())) -> inter{AC,#}(x10,empty())
   inter{AC,#}(x11,interAC(x,unionAC(y,z))) -> inter{AC,#}(x,z)
   inter{AC,#}(x11,interAC(x,unionAC(y,z))) -> inter{AC,#}(x,y)
   inter{AC,#}(x11,interAC(x,unionAC(y,z))) -> union{AC,#}(interAC(x,y),interAC(x,z))
   inter{AC,#}(x11,interAC(x,unionAC(y,z))) -> inter{AC,#}(x11,unionAC(interAC(x,y),interAC(x,z)))
   inter{AC,#}(x12,interAC(single(x),single(y))) -> eq{AC,#}(x,y)
   inter{AC,#}(x12,interAC(single(x),single(y))) -> if#(eqAC(x,y),single(x),empty())
   inter{AC,#}(x12,interAC(single(x),single(y))) ->
   inter{AC,#}(x12,if(eqAC(x,y),single(x),empty()))
  Equations:
   eqAC(eqAC(x3,x4),x5) -> eqAC(x3,eqAC(x4,x5))
   eqAC(x3,x4) -> eqAC(x4,x3)
   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)
   eqAC(x3,eqAC(x4,x5)) -> eqAC(eqAC(x3,x4),x5)
   eqAC(x4,x3) -> eqAC(x3,x4)
   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
   eqAC(0(),0()) -> true()
   eqAC(0(),1()) -> false()
   eqAC(1(),1()) -> true()
   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(eqAC(x,y),single(x),empty())
  S:
   eq{AC,#}(eqAC(x13,x14),x15) -> eq{AC,#}(x13,x14)
   eq{AC,#}(x13,eqAC(x14,x15)) -> eq{AC,#}(x14,x15)
   union{AC,#}(unionAC(x13,x14),x15) -> union{AC,#}(x13,x14)
   union{AC,#}(x13,unionAC(x14,x15)) -> union{AC,#}(x14,x15)
   inter{AC,#}(interAC(x13,x14),x15) -> inter{AC,#}(x13,x14)
   inter{AC,#}(x13,interAC(x14,x15)) -> inter{AC,#}(x14,x15)
  AC-EDG Processor:
   Equations#:
    eq{AC,#}(eqAC(x3,x4),x5) -> eq{AC,#}(x3,eqAC(x4,x5))
    eq{AC,#}(x3,x4) -> eq{AC,#}(x4,x3)
    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)
    eq{AC,#}(x3,eqAC(x4,x5)) -> eq{AC,#}(eqAC(x3,x4),x5)
    eq{AC,#}(x4,x3) -> eq{AC,#}(x3,x4)
    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:
    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{AC,#}(x,y)
    inter{AC,#}(single(x),single(y)) -> if#(eqAC(x,y),single(x),empty())
    eq{AC,#}(x6,eqAC(0(),0())) -> eq{AC,#}(x6,true())
    eq{AC,#}(x7,eqAC(0(),1())) -> eq{AC,#}(x7,false())
    eq{AC,#}(x8,eqAC(1(),1())) -> eq{AC,#}(x8,true())
    union{AC,#}(x9,unionAC(empty(),x)) -> union{AC,#}(x9,x)
    inter{AC,#}(x10,interAC(x,empty())) -> inter{AC,#}(x10,empty())
    inter{AC,#}(x11,interAC(x,unionAC(y,z))) -> inter{AC,#}(x,z)
    inter{AC,#}(x11,interAC(x,unionAC(y,z))) -> inter{AC,#}(x,y)
    inter{AC,#}(x11,interAC(x,unionAC(y,z))) -> union{AC,#}(interAC(x,y),interAC(x,z))
    inter{AC,#}(x11,interAC(x,unionAC(y,z))) -> inter{AC,#}(x11,unionAC(interAC(x,y),interAC(x,z)))
    inter{AC,#}(x12,interAC(single(x),single(y))) -> eq{AC,#}(x,y)
    inter{AC,#}(x12,interAC(single(x),single(y))) -> if#(eqAC(x,y),single(x),empty())
    inter{AC,#}(x12,interAC(single(x),single(y))) ->
    inter{AC,#}(x12,if(eqAC(x,y),single(x),empty()))
   Equations:
    eqAC(eqAC(x3,x4),x5) -> eqAC(x3,eqAC(x4,x5))
    eqAC(x3,x4) -> eqAC(x4,x3)
    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)
    eqAC(x3,eqAC(x4,x5)) -> eqAC(eqAC(x3,x4),x5)
    eqAC(x4,x3) -> eqAC(x3,x4)
    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
    eqAC(0(),0()) -> true()
    eqAC(0(),1()) -> false()
    eqAC(1(),1()) -> true()
    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(eqAC(x,y),single(x),empty())
   S:
    eq{AC,#}(eqAC(x13,x14),x15) -> eq{AC,#}(x13,x14)
    eq{AC,#}(x13,eqAC(x14,x15)) -> eq{AC,#}(x14,x15)
    union{AC,#}(unionAC(x13,x14),x15) -> union{AC,#}(x13,x14)
    union{AC,#}(x13,unionAC(x14,x15)) -> union{AC,#}(x14,x15)
    inter{AC,#}(interAC(x13,x14),x15) -> inter{AC,#}(x13,x14)
    inter{AC,#}(x13,interAC(x14,x15)) -> inter{AC,#}(x14,x15)
   Open