YES
Time: 0.837

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)
   SCC Processor:
    #sccs: 3
    #rules: 11
    #arcs: 109/289
    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,#}(x12,interAC(single(x),single(y))) ->
     inter{AC,#}(x12,if(eqAC(x,y),single(x),empty()))
     inter{AC,#}(x11,interAC(x,unionAC(y,z))) ->
     inter{AC,#}(x11,unionAC(interAC(x,y),interAC(x,z)))
     inter{AC,#}(x11,interAC(x,unionAC(y,z))) -> inter{AC,#}(x,y)
     inter{AC,#}(x11,interAC(x,unionAC(y,z))) -> inter{AC,#}(x,z)
     inter{AC,#}(x10,interAC(x,empty())) -> inter{AC,#}(x10,empty())
     inter{AC,#}(x,unionAC(y,z)) -> inter{AC,#}(x,y)
     inter{AC,#}(x,unionAC(y,z)) -> inter{AC,#}(x,z)
    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-DP unlabeling:
     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)
     DPs:
      interAC(x12,interAC(single(x),single(y))) -> interAC(x12,if(eqAC(x,y),single(x),empty()))
      interAC(x11,interAC(x,unionAC(y,z))) -> interAC(x11,unionAC(interAC(x,y),interAC(x,z)))
      interAC(x11,interAC(x,unionAC(y,z))) -> interAC(x,y)
      interAC(x11,interAC(x,unionAC(y,z))) -> interAC(x,z)
      interAC(x10,interAC(x,empty())) -> interAC(x10,empty())
      interAC(x,unionAC(y,z)) -> interAC(x,y)
      interAC(x,unionAC(y,z)) -> interAC(x,z)
     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:
      eqAC(eqAC(x13,x14),x15) -> eqAC(x13,x14)
      eqAC(x13,eqAC(x14,x15)) -> eqAC(x14,x15)
      unionAC(unionAC(x13,x14),x15) -> unionAC(x13,x14)
      unionAC(x13,unionAC(x14,x15)) -> unionAC(x14,x15)
      interAC(interAC(x13,x14),x15) -> interAC(x13,x14)
      interAC(x13,interAC(x14,x15)) -> interAC(x14,x15)
     AC-RPO Processor:
      argument filtering:
       pi(unionAC) = [0,1]
       pi(interAC) = [0,1]
       pi(eqAC) = []
       pi(true) = []
       pi(if) = [1,2]
       pi(false) = []
       pi(0) = []
       pi(1) = []
       pi(empty) = []
       pi(single) = [0]
      precedence:
       true > interAC > if > single > empty > false > 1 > unionAC > 0 > eqAC
      status:
       if:mul  
      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)
       DPs:
        
       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:
        eqAC(eqAC(x13,x14),x15) -> eqAC(x13,x14)
        eqAC(x13,eqAC(x14,x15)) -> eqAC(x14,x15)
        unionAC(unionAC(x13,x14),x15) -> unionAC(x13,x14)
        unionAC(x13,unionAC(x14,x15)) -> unionAC(x14,x15)
        interAC(interAC(x13,x14),x15) -> interAC(x13,x14)
        interAC(x13,interAC(x14,x15)) -> interAC(x14,x15)
      Qed
    
    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:
     union{AC,#}(x9,unionAC(empty(),x)) -> union{AC,#}(x9,x)
    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-DP unlabeling:
     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)
     DPs:
      unionAC(x9,unionAC(empty(),x)) -> unionAC(x9,x)
     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:
      eqAC(eqAC(x13,x14),x15) -> eqAC(x13,x14)
      eqAC(x13,eqAC(x14,x15)) -> eqAC(x14,x15)
      unionAC(unionAC(x13,x14),x15) -> unionAC(x13,x14)
      unionAC(x13,unionAC(x14,x15)) -> unionAC(x14,x15)
      interAC(interAC(x13,x14),x15) -> interAC(x13,x14)
      interAC(x13,interAC(x14,x15)) -> interAC(x14,x15)
     Usable Rule Processor:
      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)
      DPs:
       unionAC(x9,unionAC(empty(),x)) -> unionAC(x9,x)
      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:
       unionAC(empty(),x) -> x
      S:
       eqAC(eqAC(x13,x14),x15) -> eqAC(x13,x14)
       eqAC(x13,eqAC(x14,x15)) -> eqAC(x14,x15)
       unionAC(unionAC(x13,x14),x15) -> unionAC(x13,x14)
       unionAC(x13,unionAC(x14,x15)) -> unionAC(x14,x15)
       interAC(interAC(x13,x14),x15) -> interAC(x13,x14)
       interAC(x13,interAC(x14,x15)) -> interAC(x14,x15)
      AC-RPO Processor:
       argument filtering:
        pi(unionAC) = [0,1]
        pi(interAC) = []
        pi(eqAC) = []
        pi(empty) = []
       precedence:
        empty > eqAC > interAC > unionAC
       status:
        
       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)
        DPs:
         
        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:
         unionAC(empty(),x) -> x
        S:
         eqAC(eqAC(x13,x14),x15) -> eqAC(x13,x14)
         eqAC(x13,eqAC(x14,x15)) -> eqAC(x14,x15)
         unionAC(unionAC(x13,x14),x15) -> unionAC(x13,x14)
         unionAC(x13,unionAC(x14,x15)) -> unionAC(x14,x15)
         interAC(interAC(x13,x14),x15) -> interAC(x13,x14)
         interAC(x13,interAC(x14,x15)) -> interAC(x14,x15)
       Qed
    
    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:
     eq{AC,#}(x8,eqAC(1(),1())) -> eq{AC,#}(x8,true())
     eq{AC,#}(x7,eqAC(0(),1())) -> eq{AC,#}(x7,false())
     eq{AC,#}(x6,eqAC(0(),0())) -> eq{AC,#}(x6,true())
    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-DP unlabeling:
     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)
     DPs:
      eqAC(x8,eqAC(1(),1())) -> eqAC(x8,true())
      eqAC(x7,eqAC(0(),1())) -> eqAC(x7,false())
      eqAC(x6,eqAC(0(),0())) -> eqAC(x6,true())
     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:
      eqAC(eqAC(x13,x14),x15) -> eqAC(x13,x14)
      eqAC(x13,eqAC(x14,x15)) -> eqAC(x14,x15)
      unionAC(unionAC(x13,x14),x15) -> unionAC(x13,x14)
      unionAC(x13,unionAC(x14,x15)) -> unionAC(x14,x15)
      interAC(interAC(x13,x14),x15) -> interAC(x13,x14)
      interAC(x13,interAC(x14,x15)) -> interAC(x14,x15)
     Usable Rule Processor:
      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)
      DPs:
       eqAC(x8,eqAC(1(),1())) -> eqAC(x8,true())
       eqAC(x7,eqAC(0(),1())) -> eqAC(x7,false())
       eqAC(x6,eqAC(0(),0())) -> eqAC(x6,true())
      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:
       
      S:
       eqAC(eqAC(x13,x14),x15) -> eqAC(x13,x14)
       eqAC(x13,eqAC(x14,x15)) -> eqAC(x14,x15)
       unionAC(unionAC(x13,x14),x15) -> unionAC(x13,x14)
       unionAC(x13,unionAC(x14,x15)) -> unionAC(x14,x15)
       interAC(interAC(x13,x14),x15) -> interAC(x13,x14)
       interAC(x13,interAC(x14,x15)) -> interAC(x14,x15)
      AC-RPO Processor:
       argument filtering:
        pi(unionAC) = [0,1]
        pi(interAC) = [0,1]
        pi(eqAC) = [0,1]
        pi(true) = []
        pi(false) = []
        pi(0) = []
        pi(1) = []
       precedence:
        unionAC > 1 > 0 > eqAC > false > interAC > true
       status:
        
       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)
        DPs:
         
        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:
         
        S:
         eqAC(eqAC(x13,x14),x15) -> eqAC(x13,x14)
         eqAC(x13,eqAC(x14,x15)) -> eqAC(x14,x15)
         unionAC(unionAC(x13,x14),x15) -> unionAC(x13,x14)
         unionAC(x13,unionAC(x14,x15)) -> unionAC(x14,x15)
         interAC(interAC(x13,x14),x15) -> interAC(x13,x14)
         interAC(x13,interAC(x14,x15)) -> interAC(x14,x15)
       Qed