YES
Time: 0.313

Problem:
 Equations:
  andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
  andAC(x3,x4) -> andAC(x4,x3)
  orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
  orAC(x3,x4) -> orAC(x4,x3)
  andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
  andAC(x4,x3) -> andAC(x3,x4)
  orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
  orAC(x4,x3) -> orAC(x3,x4)
 TRS:
  eqC(x,x) -> true()
  not(eqC(x,y)) -> neqC(x,y)
  not(neqC(x,y)) -> eqC(x,y)
  not(true()) -> false()
  not(false()) -> true()
  not(not(x)) -> x
  not(andAC(x,y)) -> orAC(not(x),not(y))
  not(orAC(x,y)) -> andAC(not(x),not(y))
  neqC(x,x) -> false()
  orAC(andAC(x,y),z) -> andAC(orAC(x,z),orAC(y,z))
  orAC(x,x) -> x
  orAC(x,true()) -> true()
  orAC(x,false()) -> x
  andAC(x,x) -> x
  andAC(x,true()) -> x
  andAC(x,false()) -> false()
  andAC(x,orAC(x,y)) -> x

Proof:
 DP Processor:
  Equations#:
   and{AC,#}(andAC(x3,x4),x5) -> and{AC,#}(x3,andAC(x4,x5))
   and{AC,#}(x3,x4) -> and{AC,#}(x4,x3)
   or{AC,#}(orAC(x3,x4),x5) -> or{AC,#}(x3,orAC(x4,x5))
   or{AC,#}(x3,x4) -> or{AC,#}(x4,x3)
   and{AC,#}(x3,andAC(x4,x5)) -> and{AC,#}(andAC(x3,x4),x5)
   and{AC,#}(x4,x3) -> and{AC,#}(x3,x4)
   or{AC,#}(x3,orAC(x4,x5)) -> or{AC,#}(orAC(x3,x4),x5)
   or{AC,#}(x4,x3) -> or{AC,#}(x3,x4)
  DPs:
   not#(eqC(x,y)) -> neq{C,#}(x,y)
   not#(neqC(x,y)) -> eq{C,#}(x,y)
   not#(andAC(x,y)) -> not#(y)
   not#(andAC(x,y)) -> not#(x)
   not#(andAC(x,y)) -> or{AC,#}(not(x),not(y))
   not#(orAC(x,y)) -> not#(y)
   not#(orAC(x,y)) -> not#(x)
   not#(orAC(x,y)) -> and{AC,#}(not(x),not(y))
   or{AC,#}(andAC(x,y),z) -> or{AC,#}(y,z)
   or{AC,#}(andAC(x,y),z) -> or{AC,#}(x,z)
   or{AC,#}(andAC(x,y),z) -> and{AC,#}(orAC(x,z),orAC(y,z))
   or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(y,z)
   or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(x,z)
   or{AC,#}(x6,orAC(andAC(x,y),z)) -> and{AC,#}(orAC(x,z),orAC(y,z))
   or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(x6,andAC(orAC(x,z),orAC(y,z)))
   or{AC,#}(x7,orAC(x,x)) -> or{AC,#}(x7,x)
   or{AC,#}(x8,orAC(x,true())) -> or{AC,#}(x8,true())
   or{AC,#}(x9,orAC(x,false())) -> or{AC,#}(x9,x)
   and{AC,#}(x10,andAC(x,x)) -> and{AC,#}(x10,x)
   and{AC,#}(x11,andAC(x,true())) -> and{AC,#}(x11,x)
   and{AC,#}(x12,andAC(x,false())) -> and{AC,#}(x12,false())
   and{AC,#}(x13,andAC(x,orAC(x,y))) -> and{AC,#}(x13,x)
  Equations:
   andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
   andAC(x3,x4) -> andAC(x4,x3)
   orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
   orAC(x3,x4) -> orAC(x4,x3)
   andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
   andAC(x4,x3) -> andAC(x3,x4)
   orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
   orAC(x4,x3) -> orAC(x3,x4)
  TRS:
   eqC(x,x) -> true()
   not(eqC(x,y)) -> neqC(x,y)
   not(neqC(x,y)) -> eqC(x,y)
   not(true()) -> false()
   not(false()) -> true()
   not(not(x)) -> x
   not(andAC(x,y)) -> orAC(not(x),not(y))
   not(orAC(x,y)) -> andAC(not(x),not(y))
   neqC(x,x) -> false()
   orAC(andAC(x,y),z) -> andAC(orAC(x,z),orAC(y,z))
   orAC(x,x) -> x
   orAC(x,true()) -> true()
   orAC(x,false()) -> x
   andAC(x,x) -> x
   andAC(x,true()) -> x
   andAC(x,false()) -> false()
   andAC(x,orAC(x,y)) -> x
  S:
   and{AC,#}(andAC(x14,x15),x16) -> and{AC,#}(x14,x15)
   and{AC,#}(x14,andAC(x15,x16)) -> and{AC,#}(x15,x16)
   or{AC,#}(orAC(x14,x15),x16) -> or{AC,#}(x14,x15)
   or{AC,#}(x14,orAC(x15,x16)) -> or{AC,#}(x15,x16)
  AC-EDG Processor:
   Equations#:
    and{AC,#}(andAC(x3,x4),x5) -> and{AC,#}(x3,andAC(x4,x5))
    and{AC,#}(x3,x4) -> and{AC,#}(x4,x3)
    or{AC,#}(orAC(x3,x4),x5) -> or{AC,#}(x3,orAC(x4,x5))
    or{AC,#}(x3,x4) -> or{AC,#}(x4,x3)
    and{AC,#}(x3,andAC(x4,x5)) -> and{AC,#}(andAC(x3,x4),x5)
    and{AC,#}(x4,x3) -> and{AC,#}(x3,x4)
    or{AC,#}(x3,orAC(x4,x5)) -> or{AC,#}(orAC(x3,x4),x5)
    or{AC,#}(x4,x3) -> or{AC,#}(x3,x4)
   DPs:
    not#(eqC(x,y)) -> neq{C,#}(x,y)
    not#(neqC(x,y)) -> eq{C,#}(x,y)
    not#(andAC(x,y)) -> not#(y)
    not#(andAC(x,y)) -> not#(x)
    not#(andAC(x,y)) -> or{AC,#}(not(x),not(y))
    not#(orAC(x,y)) -> not#(y)
    not#(orAC(x,y)) -> not#(x)
    not#(orAC(x,y)) -> and{AC,#}(not(x),not(y))
    or{AC,#}(andAC(x,y),z) -> or{AC,#}(y,z)
    or{AC,#}(andAC(x,y),z) -> or{AC,#}(x,z)
    or{AC,#}(andAC(x,y),z) -> and{AC,#}(orAC(x,z),orAC(y,z))
    or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(y,z)
    or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(x,z)
    or{AC,#}(x6,orAC(andAC(x,y),z)) -> and{AC,#}(orAC(x,z),orAC(y,z))
    or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(x6,andAC(orAC(x,z),orAC(y,z)))
    or{AC,#}(x7,orAC(x,x)) -> or{AC,#}(x7,x)
    or{AC,#}(x8,orAC(x,true())) -> or{AC,#}(x8,true())
    or{AC,#}(x9,orAC(x,false())) -> or{AC,#}(x9,x)
    and{AC,#}(x10,andAC(x,x)) -> and{AC,#}(x10,x)
    and{AC,#}(x11,andAC(x,true())) -> and{AC,#}(x11,x)
    and{AC,#}(x12,andAC(x,false())) -> and{AC,#}(x12,false())
    and{AC,#}(x13,andAC(x,orAC(x,y))) -> and{AC,#}(x13,x)
   Equations:
    andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
    andAC(x3,x4) -> andAC(x4,x3)
    orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
    orAC(x3,x4) -> orAC(x4,x3)
    andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
    andAC(x4,x3) -> andAC(x3,x4)
    orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
    orAC(x4,x3) -> orAC(x3,x4)
   TRS:
    eqC(x,x) -> true()
    not(eqC(x,y)) -> neqC(x,y)
    not(neqC(x,y)) -> eqC(x,y)
    not(true()) -> false()
    not(false()) -> true()
    not(not(x)) -> x
    not(andAC(x,y)) -> orAC(not(x),not(y))
    not(orAC(x,y)) -> andAC(not(x),not(y))
    neqC(x,x) -> false()
    orAC(andAC(x,y),z) -> andAC(orAC(x,z),orAC(y,z))
    orAC(x,x) -> x
    orAC(x,true()) -> true()
    orAC(x,false()) -> x
    andAC(x,x) -> x
    andAC(x,true()) -> x
    andAC(x,false()) -> false()
    andAC(x,orAC(x,y)) -> x
   S:
    and{AC,#}(andAC(x14,x15),x16) -> and{AC,#}(x14,x15)
    and{AC,#}(x14,andAC(x15,x16)) -> and{AC,#}(x15,x16)
    or{AC,#}(orAC(x14,x15),x16) -> or{AC,#}(x14,x15)
    or{AC,#}(x14,orAC(x15,x16)) -> or{AC,#}(x15,x16)
   SCC Processor:
    #sccs: 3
    #rules: 16
    #arcs: 150/484
    Equations#:
     and{AC,#}(andAC(x3,x4),x5) -> and{AC,#}(x3,andAC(x4,x5))
     and{AC,#}(x3,x4) -> and{AC,#}(x4,x3)
     or{AC,#}(orAC(x3,x4),x5) -> or{AC,#}(x3,orAC(x4,x5))
     or{AC,#}(x3,x4) -> or{AC,#}(x4,x3)
     and{AC,#}(x3,andAC(x4,x5)) -> and{AC,#}(andAC(x3,x4),x5)
     and{AC,#}(x4,x3) -> and{AC,#}(x3,x4)
     or{AC,#}(x3,orAC(x4,x5)) -> or{AC,#}(orAC(x3,x4),x5)
     or{AC,#}(x4,x3) -> or{AC,#}(x3,x4)
    DPs:
     not#(andAC(x,y)) -> not#(y)
     not#(orAC(x,y)) -> not#(x)
     not#(orAC(x,y)) -> not#(y)
     not#(andAC(x,y)) -> not#(x)
    Equations:
     andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
     andAC(x3,x4) -> andAC(x4,x3)
     orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
     orAC(x3,x4) -> orAC(x4,x3)
     andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
     andAC(x4,x3) -> andAC(x3,x4)
     orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
     orAC(x4,x3) -> orAC(x3,x4)
    TRS:
     eqC(x,x) -> true()
     not(eqC(x,y)) -> neqC(x,y)
     not(neqC(x,y)) -> eqC(x,y)
     not(true()) -> false()
     not(false()) -> true()
     not(not(x)) -> x
     not(andAC(x,y)) -> orAC(not(x),not(y))
     not(orAC(x,y)) -> andAC(not(x),not(y))
     neqC(x,x) -> false()
     orAC(andAC(x,y),z) -> andAC(orAC(x,z),orAC(y,z))
     orAC(x,x) -> x
     orAC(x,true()) -> true()
     orAC(x,false()) -> x
     andAC(x,x) -> x
     andAC(x,true()) -> x
     andAC(x,false()) -> false()
     andAC(x,orAC(x,y)) -> x
    S:
     and{AC,#}(andAC(x14,x15),x16) -> and{AC,#}(x14,x15)
     and{AC,#}(x14,andAC(x15,x16)) -> and{AC,#}(x15,x16)
     or{AC,#}(orAC(x14,x15),x16) -> or{AC,#}(x14,x15)
     or{AC,#}(x14,orAC(x15,x16)) -> or{AC,#}(x15,x16)
    AC-DP unlabeling:
     Equations#:
      andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
      andAC(x3,x4) -> andAC(x4,x3)
      orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
      orAC(x3,x4) -> orAC(x4,x3)
      andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
      andAC(x4,x3) -> andAC(x3,x4)
      orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
      orAC(x4,x3) -> orAC(x3,x4)
     DPs:
      not#(andAC(x,y)) -> not#(y)
      not#(orAC(x,y)) -> not#(x)
      not#(orAC(x,y)) -> not#(y)
      not#(andAC(x,y)) -> not#(x)
     Equations:
      andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
      andAC(x3,x4) -> andAC(x4,x3)
      orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
      orAC(x3,x4) -> orAC(x4,x3)
      andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
      andAC(x4,x3) -> andAC(x3,x4)
      orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
      orAC(x4,x3) -> orAC(x3,x4)
     TRS:
      eqC(x,x) -> true()
      not(eqC(x,y)) -> neqC(x,y)
      not(neqC(x,y)) -> eqC(x,y)
      not(true()) -> false()
      not(false()) -> true()
      not(not(x)) -> x
      not(andAC(x,y)) -> orAC(not(x),not(y))
      not(orAC(x,y)) -> andAC(not(x),not(y))
      neqC(x,x) -> false()
      orAC(andAC(x,y),z) -> andAC(orAC(x,z),orAC(y,z))
      orAC(x,x) -> x
      orAC(x,true()) -> true()
      orAC(x,false()) -> x
      andAC(x,x) -> x
      andAC(x,true()) -> x
      andAC(x,false()) -> false()
      andAC(x,orAC(x,y)) -> x
     S:
      andAC(andAC(x14,x15),x16) -> andAC(x14,x15)
      andAC(x14,andAC(x15,x16)) -> andAC(x15,x16)
      orAC(orAC(x14,x15),x16) -> orAC(x14,x15)
      orAC(x14,orAC(x15,x16)) -> orAC(x15,x16)
     Usable Rule Processor:
      Equations#:
       andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
       andAC(x3,x4) -> andAC(x4,x3)
       orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
       orAC(x3,x4) -> orAC(x4,x3)
       andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
       andAC(x4,x3) -> andAC(x3,x4)
       orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
       orAC(x4,x3) -> orAC(x3,x4)
      DPs:
       not#(andAC(x,y)) -> not#(y)
       not#(orAC(x,y)) -> not#(x)
       not#(orAC(x,y)) -> not#(y)
       not#(andAC(x,y)) -> not#(x)
      Equations:
       andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
       andAC(x3,x4) -> andAC(x4,x3)
       orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
       orAC(x3,x4) -> orAC(x4,x3)
       andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
       andAC(x4,x3) -> andAC(x3,x4)
       orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
       orAC(x4,x3) -> orAC(x3,x4)
      TRS:
       
      S:
       andAC(andAC(x14,x15),x16) -> andAC(x14,x15)
       andAC(x14,andAC(x15,x16)) -> andAC(x15,x16)
       orAC(orAC(x14,x15),x16) -> orAC(x14,x15)
       orAC(x14,orAC(x15,x16)) -> orAC(x15,x16)
      AC-RPO Processor:
       argument filtering:
        pi(orAC) = [0,1]
        pi(andAC) = [0,1]
        pi(not#) = [0]
       precedence:
        andAC > orAC > not#
       status:
        
       problem:
        Equations#:
         andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
         andAC(x3,x4) -> andAC(x4,x3)
         orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
         orAC(x3,x4) -> orAC(x4,x3)
         andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
         andAC(x4,x3) -> andAC(x3,x4)
         orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
         orAC(x4,x3) -> orAC(x3,x4)
        DPs:
         
        Equations:
         andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
         andAC(x3,x4) -> andAC(x4,x3)
         orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
         orAC(x3,x4) -> orAC(x4,x3)
         andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
         andAC(x4,x3) -> andAC(x3,x4)
         orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
         orAC(x4,x3) -> orAC(x3,x4)
        TRS:
         
        S:
         andAC(andAC(x14,x15),x16) -> andAC(x14,x15)
         andAC(x14,andAC(x15,x16)) -> andAC(x15,x16)
         orAC(orAC(x14,x15),x16) -> orAC(x14,x15)
         orAC(x14,orAC(x15,x16)) -> orAC(x15,x16)
       Qed
    
    Equations#:
     and{AC,#}(andAC(x3,x4),x5) -> and{AC,#}(x3,andAC(x4,x5))
     and{AC,#}(x3,x4) -> and{AC,#}(x4,x3)
     or{AC,#}(orAC(x3,x4),x5) -> or{AC,#}(x3,orAC(x4,x5))
     or{AC,#}(x3,x4) -> or{AC,#}(x4,x3)
     and{AC,#}(x3,andAC(x4,x5)) -> and{AC,#}(andAC(x3,x4),x5)
     and{AC,#}(x4,x3) -> and{AC,#}(x3,x4)
     or{AC,#}(x3,orAC(x4,x5)) -> or{AC,#}(orAC(x3,x4),x5)
     or{AC,#}(x4,x3) -> or{AC,#}(x3,x4)
    DPs:
     or{AC,#}(andAC(x,y),z) -> or{AC,#}(y,z)
     or{AC,#}(x9,orAC(x,false())) -> or{AC,#}(x9,x)
     or{AC,#}(x8,orAC(x,true())) -> or{AC,#}(x8,true())
     or{AC,#}(x7,orAC(x,x)) -> or{AC,#}(x7,x)
     or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(x6,andAC(orAC(x,z),orAC(y,z)))
     or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(x,z)
     or{AC,#}(x6,orAC(andAC(x,y),z)) -> or{AC,#}(y,z)
     or{AC,#}(andAC(x,y),z) -> or{AC,#}(x,z)
    Equations:
     andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
     andAC(x3,x4) -> andAC(x4,x3)
     orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
     orAC(x3,x4) -> orAC(x4,x3)
     andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
     andAC(x4,x3) -> andAC(x3,x4)
     orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
     orAC(x4,x3) -> orAC(x3,x4)
    TRS:
     eqC(x,x) -> true()
     not(eqC(x,y)) -> neqC(x,y)
     not(neqC(x,y)) -> eqC(x,y)
     not(true()) -> false()
     not(false()) -> true()
     not(not(x)) -> x
     not(andAC(x,y)) -> orAC(not(x),not(y))
     not(orAC(x,y)) -> andAC(not(x),not(y))
     neqC(x,x) -> false()
     orAC(andAC(x,y),z) -> andAC(orAC(x,z),orAC(y,z))
     orAC(x,x) -> x
     orAC(x,true()) -> true()
     orAC(x,false()) -> x
     andAC(x,x) -> x
     andAC(x,true()) -> x
     andAC(x,false()) -> false()
     andAC(x,orAC(x,y)) -> x
    S:
     and{AC,#}(andAC(x14,x15),x16) -> and{AC,#}(x14,x15)
     and{AC,#}(x14,andAC(x15,x16)) -> and{AC,#}(x15,x16)
     or{AC,#}(orAC(x14,x15),x16) -> or{AC,#}(x14,x15)
     or{AC,#}(x14,orAC(x15,x16)) -> or{AC,#}(x15,x16)
    AC-DP unlabeling:
     Equations#:
      andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
      andAC(x3,x4) -> andAC(x4,x3)
      orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
      orAC(x3,x4) -> orAC(x4,x3)
      andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
      andAC(x4,x3) -> andAC(x3,x4)
      orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
      orAC(x4,x3) -> orAC(x3,x4)
     DPs:
      orAC(andAC(x,y),z) -> orAC(y,z)
      orAC(x9,orAC(x,false())) -> orAC(x9,x)
      orAC(x8,orAC(x,true())) -> orAC(x8,true())
      orAC(x7,orAC(x,x)) -> orAC(x7,x)
      orAC(x6,orAC(andAC(x,y),z)) -> orAC(x6,andAC(orAC(x,z),orAC(y,z)))
      orAC(x6,orAC(andAC(x,y),z)) -> orAC(x,z)
      orAC(x6,orAC(andAC(x,y),z)) -> orAC(y,z)
      orAC(andAC(x,y),z) -> orAC(x,z)
     Equations:
      andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
      andAC(x3,x4) -> andAC(x4,x3)
      orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
      orAC(x3,x4) -> orAC(x4,x3)
      andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
      andAC(x4,x3) -> andAC(x3,x4)
      orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
      orAC(x4,x3) -> orAC(x3,x4)
     TRS:
      eqC(x,x) -> true()
      not(eqC(x,y)) -> neqC(x,y)
      not(neqC(x,y)) -> eqC(x,y)
      not(true()) -> false()
      not(false()) -> true()
      not(not(x)) -> x
      not(andAC(x,y)) -> orAC(not(x),not(y))
      not(orAC(x,y)) -> andAC(not(x),not(y))
      neqC(x,x) -> false()
      orAC(andAC(x,y),z) -> andAC(orAC(x,z),orAC(y,z))
      orAC(x,x) -> x
      orAC(x,true()) -> true()
      orAC(x,false()) -> x
      andAC(x,x) -> x
      andAC(x,true()) -> x
      andAC(x,false()) -> false()
      andAC(x,orAC(x,y)) -> x
     S:
      andAC(andAC(x14,x15),x16) -> andAC(x14,x15)
      andAC(x14,andAC(x15,x16)) -> andAC(x15,x16)
      orAC(orAC(x14,x15),x16) -> orAC(x14,x15)
      orAC(x14,orAC(x15,x16)) -> orAC(x15,x16)
     Usable Rule Processor:
      Equations#:
       andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
       andAC(x3,x4) -> andAC(x4,x3)
       orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
       orAC(x3,x4) -> orAC(x4,x3)
       andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
       andAC(x4,x3) -> andAC(x3,x4)
       orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
       orAC(x4,x3) -> orAC(x3,x4)
      DPs:
       orAC(andAC(x,y),z) -> orAC(y,z)
       orAC(x9,orAC(x,false())) -> orAC(x9,x)
       orAC(x8,orAC(x,true())) -> orAC(x8,true())
       orAC(x7,orAC(x,x)) -> orAC(x7,x)
       orAC(x6,orAC(andAC(x,y),z)) -> orAC(x6,andAC(orAC(x,z),orAC(y,z)))
       orAC(x6,orAC(andAC(x,y),z)) -> orAC(x,z)
       orAC(x6,orAC(andAC(x,y),z)) -> orAC(y,z)
       orAC(andAC(x,y),z) -> orAC(x,z)
      Equations:
       andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
       andAC(x3,x4) -> andAC(x4,x3)
       orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
       orAC(x3,x4) -> orAC(x4,x3)
       andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
       andAC(x4,x3) -> andAC(x3,x4)
       orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
       orAC(x4,x3) -> orAC(x3,x4)
      TRS:
       orAC(andAC(x,y),z) -> andAC(orAC(x,z),orAC(y,z))
       orAC(x,x) -> x
       orAC(x,true()) -> true()
       orAC(x,false()) -> x
       andAC(x,x) -> x
       andAC(x,true()) -> x
       andAC(x,false()) -> false()
       andAC(x,orAC(x,y)) -> x
      S:
       andAC(andAC(x14,x15),x16) -> andAC(x14,x15)
       andAC(x14,andAC(x15,x16)) -> andAC(x15,x16)
       orAC(orAC(x14,x15),x16) -> orAC(x14,x15)
       orAC(x14,orAC(x15,x16)) -> orAC(x15,x16)
      AC-RPO Processor:
       argument filtering:
        pi(orAC) = [0,1]
        pi(andAC) = [0,1]
        pi(true) = []
        pi(false) = []
       precedence:
        orAC > true > andAC > false
       status:
        
       problem:
        Equations#:
         andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
         andAC(x3,x4) -> andAC(x4,x3)
         orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
         orAC(x3,x4) -> orAC(x4,x3)
         andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
         andAC(x4,x3) -> andAC(x3,x4)
         orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
         orAC(x4,x3) -> orAC(x3,x4)
        DPs:
         
        Equations:
         andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
         andAC(x3,x4) -> andAC(x4,x3)
         orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
         orAC(x3,x4) -> orAC(x4,x3)
         andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
         andAC(x4,x3) -> andAC(x3,x4)
         orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
         orAC(x4,x3) -> orAC(x3,x4)
        TRS:
         orAC(andAC(x,y),z) -> andAC(orAC(x,z),orAC(y,z))
         orAC(x,x) -> x
         orAC(x,true()) -> true()
         orAC(x,false()) -> x
         andAC(x,x) -> x
         andAC(x,true()) -> x
         andAC(x,false()) -> false()
         andAC(x,orAC(x,y)) -> x
        S:
         andAC(andAC(x14,x15),x16) -> andAC(x14,x15)
         andAC(x14,andAC(x15,x16)) -> andAC(x15,x16)
         orAC(orAC(x14,x15),x16) -> orAC(x14,x15)
         orAC(x14,orAC(x15,x16)) -> orAC(x15,x16)
       Qed
    
    Equations#:
     and{AC,#}(andAC(x3,x4),x5) -> and{AC,#}(x3,andAC(x4,x5))
     and{AC,#}(x3,x4) -> and{AC,#}(x4,x3)
     or{AC,#}(orAC(x3,x4),x5) -> or{AC,#}(x3,orAC(x4,x5))
     or{AC,#}(x3,x4) -> or{AC,#}(x4,x3)
     and{AC,#}(x3,andAC(x4,x5)) -> and{AC,#}(andAC(x3,x4),x5)
     and{AC,#}(x4,x3) -> and{AC,#}(x3,x4)
     or{AC,#}(x3,orAC(x4,x5)) -> or{AC,#}(orAC(x3,x4),x5)
     or{AC,#}(x4,x3) -> or{AC,#}(x3,x4)
    DPs:
     and{AC,#}(x13,andAC(x,orAC(x,y))) -> and{AC,#}(x13,x)
     and{AC,#}(x12,andAC(x,false())) -> and{AC,#}(x12,false())
     and{AC,#}(x11,andAC(x,true())) -> and{AC,#}(x11,x)
     and{AC,#}(x10,andAC(x,x)) -> and{AC,#}(x10,x)
    Equations:
     andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
     andAC(x3,x4) -> andAC(x4,x3)
     orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
     orAC(x3,x4) -> orAC(x4,x3)
     andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
     andAC(x4,x3) -> andAC(x3,x4)
     orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
     orAC(x4,x3) -> orAC(x3,x4)
    TRS:
     eqC(x,x) -> true()
     not(eqC(x,y)) -> neqC(x,y)
     not(neqC(x,y)) -> eqC(x,y)
     not(true()) -> false()
     not(false()) -> true()
     not(not(x)) -> x
     not(andAC(x,y)) -> orAC(not(x),not(y))
     not(orAC(x,y)) -> andAC(not(x),not(y))
     neqC(x,x) -> false()
     orAC(andAC(x,y),z) -> andAC(orAC(x,z),orAC(y,z))
     orAC(x,x) -> x
     orAC(x,true()) -> true()
     orAC(x,false()) -> x
     andAC(x,x) -> x
     andAC(x,true()) -> x
     andAC(x,false()) -> false()
     andAC(x,orAC(x,y)) -> x
    S:
     and{AC,#}(andAC(x14,x15),x16) -> and{AC,#}(x14,x15)
     and{AC,#}(x14,andAC(x15,x16)) -> and{AC,#}(x15,x16)
     or{AC,#}(orAC(x14,x15),x16) -> or{AC,#}(x14,x15)
     or{AC,#}(x14,orAC(x15,x16)) -> or{AC,#}(x15,x16)
    AC-DP unlabeling:
     Equations#:
      andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
      andAC(x3,x4) -> andAC(x4,x3)
      orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
      orAC(x3,x4) -> orAC(x4,x3)
      andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
      andAC(x4,x3) -> andAC(x3,x4)
      orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
      orAC(x4,x3) -> orAC(x3,x4)
     DPs:
      andAC(x13,andAC(x,orAC(x,y))) -> andAC(x13,x)
      andAC(x12,andAC(x,false())) -> andAC(x12,false())
      andAC(x11,andAC(x,true())) -> andAC(x11,x)
      andAC(x10,andAC(x,x)) -> andAC(x10,x)
     Equations:
      andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
      andAC(x3,x4) -> andAC(x4,x3)
      orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
      orAC(x3,x4) -> orAC(x4,x3)
      andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
      andAC(x4,x3) -> andAC(x3,x4)
      orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
      orAC(x4,x3) -> orAC(x3,x4)
     TRS:
      eqC(x,x) -> true()
      not(eqC(x,y)) -> neqC(x,y)
      not(neqC(x,y)) -> eqC(x,y)
      not(true()) -> false()
      not(false()) -> true()
      not(not(x)) -> x
      not(andAC(x,y)) -> orAC(not(x),not(y))
      not(orAC(x,y)) -> andAC(not(x),not(y))
      neqC(x,x) -> false()
      orAC(andAC(x,y),z) -> andAC(orAC(x,z),orAC(y,z))
      orAC(x,x) -> x
      orAC(x,true()) -> true()
      orAC(x,false()) -> x
      andAC(x,x) -> x
      andAC(x,true()) -> x
      andAC(x,false()) -> false()
      andAC(x,orAC(x,y)) -> x
     S:
      andAC(andAC(x14,x15),x16) -> andAC(x14,x15)
      andAC(x14,andAC(x15,x16)) -> andAC(x15,x16)
      orAC(orAC(x14,x15),x16) -> orAC(x14,x15)
      orAC(x14,orAC(x15,x16)) -> orAC(x15,x16)
     Usable Rule Processor:
      Equations#:
       andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
       andAC(x3,x4) -> andAC(x4,x3)
       orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
       orAC(x3,x4) -> orAC(x4,x3)
       andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
       andAC(x4,x3) -> andAC(x3,x4)
       orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
       orAC(x4,x3) -> orAC(x3,x4)
      DPs:
       andAC(x13,andAC(x,orAC(x,y))) -> andAC(x13,x)
       andAC(x12,andAC(x,false())) -> andAC(x12,false())
       andAC(x11,andAC(x,true())) -> andAC(x11,x)
       andAC(x10,andAC(x,x)) -> andAC(x10,x)
      Equations:
       andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
       andAC(x3,x4) -> andAC(x4,x3)
       orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
       orAC(x3,x4) -> orAC(x4,x3)
       andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
       andAC(x4,x3) -> andAC(x3,x4)
       orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
       orAC(x4,x3) -> orAC(x3,x4)
      TRS:
       andAC(x,x) -> x
       andAC(x,true()) -> x
       andAC(x,false()) -> false()
       andAC(x,orAC(x,y)) -> x
      S:
       andAC(andAC(x14,x15),x16) -> andAC(x14,x15)
       andAC(x14,andAC(x15,x16)) -> andAC(x15,x16)
       orAC(orAC(x14,x15),x16) -> orAC(x14,x15)
       orAC(x14,orAC(x15,x16)) -> orAC(x15,x16)
      AC-RPO Processor:
       argument filtering:
        pi(orAC) = []
        pi(andAC) = [0,1]
        pi(true) = []
        pi(false) = []
       precedence:
        andAC > false > true > orAC
       status:
        
       problem:
        Equations#:
         andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
         andAC(x3,x4) -> andAC(x4,x3)
         orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
         orAC(x3,x4) -> orAC(x4,x3)
         andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
         andAC(x4,x3) -> andAC(x3,x4)
         orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
         orAC(x4,x3) -> orAC(x3,x4)
        DPs:
         
        Equations:
         andAC(andAC(x3,x4),x5) -> andAC(x3,andAC(x4,x5))
         andAC(x3,x4) -> andAC(x4,x3)
         orAC(orAC(x3,x4),x5) -> orAC(x3,orAC(x4,x5))
         orAC(x3,x4) -> orAC(x4,x3)
         andAC(x3,andAC(x4,x5)) -> andAC(andAC(x3,x4),x5)
         andAC(x4,x3) -> andAC(x3,x4)
         orAC(x3,orAC(x4,x5)) -> orAC(orAC(x3,x4),x5)
         orAC(x4,x3) -> orAC(x3,x4)
        TRS:
         andAC(x,x) -> x
         andAC(x,true()) -> x
         andAC(x,false()) -> false()
         andAC(x,orAC(x,y)) -> x
        S:
         andAC(andAC(x14,x15),x16) -> andAC(x14,x15)
         andAC(x14,andAC(x15,x16)) -> andAC(x15,x16)
         orAC(orAC(x14,x15),x16) -> orAC(x14,x15)
         orAC(x14,orAC(x15,x16)) -> orAC(x15,x16)
       Qed