YES
Time: 0.823

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