MAYBE
Time: 0.403

Problem:
 Equations:
  unAC(unAC(x3,x4),x5) -> unAC(x3,unAC(x4,x5))
  unAC(x3,x4) -> unAC(x4,x3)
  interAC(interAC(x3,x4),x5) -> interAC(x3,interAC(x4,x5))
  interAC(x3,x4) -> interAC(x4,x3)
  unAC(x3,unAC(x4,x5)) -> unAC(unAC(x3,x4),x5)
  unAC(x4,x3) -> unAC(x3,x4)
  interAC(x3,interAC(x4,x5)) -> interAC(interAC(x3,x4),x5)
  interAC(x4,x3) -> interAC(x3,x4)
 TRS:
  unAC(empty(),x) -> x
  if(true(),x,y) -> x
  if(false(),x,y) -> y
  eq(0(),0()) -> true()
  eq(0(),s(x)) -> false()
  eq(s(x),0()) -> false()
  eq(s(x),s(y)) -> eq(x,y)
  interAC(x,empty()) -> empty()
  interAC(x,unAC(y,z)) -> unAC(interAC(x,y),interAC(x,z))
  interAC(single(x),single(y)) -> if(eq(x,y),single(x),empty())

Proof:
 DP Processor:
  Equations#:
   un{AC,#}(unAC(x3,x4),x5) -> un{AC,#}(x3,unAC(x4,x5))
   un{AC,#}(x3,x4) -> un{AC,#}(x4,x3)
   inter{AC,#}(interAC(x3,x4),x5) -> inter{AC,#}(x3,interAC(x4,x5))
   inter{AC,#}(x3,x4) -> inter{AC,#}(x4,x3)
   un{AC,#}(x3,unAC(x4,x5)) -> un{AC,#}(unAC(x3,x4),x5)
   un{AC,#}(x4,x3) -> un{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,unAC(y,z)) -> inter{AC,#}(x,z)
   inter{AC,#}(x,unAC(y,z)) -> inter{AC,#}(x,y)
   inter{AC,#}(x,unAC(y,z)) -> un{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())
   un{AC,#}(x6,unAC(empty(),x)) -> un{AC,#}(x6,x)
   inter{AC,#}(x7,interAC(x,empty())) -> inter{AC,#}(x7,empty())
   inter{AC,#}(x8,interAC(x,unAC(y,z))) -> inter{AC,#}(x,z)
   inter{AC,#}(x8,interAC(x,unAC(y,z))) -> inter{AC,#}(x,y)
   inter{AC,#}(x8,interAC(x,unAC(y,z))) -> un{AC,#}(interAC(x,y),interAC(x,z))
   inter{AC,#}(x8,interAC(x,unAC(y,z))) -> inter{AC,#}(x8,unAC(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:
   unAC(unAC(x3,x4),x5) -> unAC(x3,unAC(x4,x5))
   unAC(x3,x4) -> unAC(x4,x3)
   interAC(interAC(x3,x4),x5) -> interAC(x3,interAC(x4,x5))
   interAC(x3,x4) -> interAC(x4,x3)
   unAC(x3,unAC(x4,x5)) -> unAC(unAC(x3,x4),x5)
   unAC(x4,x3) -> unAC(x3,x4)
   interAC(x3,interAC(x4,x5)) -> interAC(interAC(x3,x4),x5)
   interAC(x4,x3) -> interAC(x3,x4)
  TRS:
   unAC(empty(),x) -> x
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   eq(0(),0()) -> true()
   eq(0(),s(x)) -> false()
   eq(s(x),0()) -> false()
   eq(s(x),s(y)) -> eq(x,y)
   interAC(x,empty()) -> empty()
   interAC(x,unAC(y,z)) -> unAC(interAC(x,y),interAC(x,z))
   interAC(single(x),single(y)) -> if(eq(x,y),single(x),empty())
  S:
   un{AC,#}(unAC(x10,x11),x12) -> un{AC,#}(x10,x11)
   un{AC,#}(x10,unAC(x11,x12)) -> un{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#:
    un{AC,#}(unAC(x3,x4),x5) -> un{AC,#}(x3,unAC(x4,x5))
    un{AC,#}(x3,x4) -> un{AC,#}(x4,x3)
    inter{AC,#}(interAC(x3,x4),x5) -> inter{AC,#}(x3,interAC(x4,x5))
    inter{AC,#}(x3,x4) -> inter{AC,#}(x4,x3)
    un{AC,#}(x3,unAC(x4,x5)) -> un{AC,#}(unAC(x3,x4),x5)
    un{AC,#}(x4,x3) -> un{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,unAC(y,z)) -> inter{AC,#}(x,z)
    inter{AC,#}(x,unAC(y,z)) -> inter{AC,#}(x,y)
    inter{AC,#}(x,unAC(y,z)) -> un{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())
    un{AC,#}(x6,unAC(empty(),x)) -> un{AC,#}(x6,x)
    inter{AC,#}(x7,interAC(x,empty())) -> inter{AC,#}(x7,empty())
    inter{AC,#}(x8,interAC(x,unAC(y,z))) -> inter{AC,#}(x,z)
    inter{AC,#}(x8,interAC(x,unAC(y,z))) -> inter{AC,#}(x,y)
    inter{AC,#}(x8,interAC(x,unAC(y,z))) -> un{AC,#}(interAC(x,y),interAC(x,z))
    inter{AC,#}(x8,interAC(x,unAC(y,z))) -> inter{AC,#}(x8,unAC(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:
    unAC(unAC(x3,x4),x5) -> unAC(x3,unAC(x4,x5))
    unAC(x3,x4) -> unAC(x4,x3)
    interAC(interAC(x3,x4),x5) -> interAC(x3,interAC(x4,x5))
    interAC(x3,x4) -> interAC(x4,x3)
    unAC(x3,unAC(x4,x5)) -> unAC(unAC(x3,x4),x5)
    unAC(x4,x3) -> unAC(x3,x4)
    interAC(x3,interAC(x4,x5)) -> interAC(interAC(x3,x4),x5)
    interAC(x4,x3) -> interAC(x3,x4)
   TRS:
    unAC(empty(),x) -> x
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    eq(0(),0()) -> true()
    eq(0(),s(x)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    interAC(x,empty()) -> empty()
    interAC(x,unAC(y,z)) -> unAC(interAC(x,y),interAC(x,z))
    interAC(single(x),single(y)) -> if(eq(x,y),single(x),empty())
   S:
    un{AC,#}(unAC(x10,x11),x12) -> un{AC,#}(x10,x11)
    un{AC,#}(x10,unAC(x11,x12)) -> un{AC,#}(x11,x12)
    inter{AC,#}(interAC(x10,x11),x12) -> inter{AC,#}(x10,x11)
    inter{AC,#}(x10,interAC(x11,x12)) -> inter{AC,#}(x11,x12)
   Open