YES
Time: 0.079

Problem:
 Equations:
  orAC(orAC(x2,x3),x4) -> orAC(x2,orAC(x3,x4))
  orAC(x2,x3) -> orAC(x3,x2)
  andAC(andAC(x2,x3),x4) -> andAC(x2,andAC(x3,x4))
  andAC(x2,x3) -> andAC(x3,x2)
  orAC(x2,orAC(x3,x4)) -> orAC(orAC(x2,x3),x4)
  orAC(x3,x2) -> orAC(x2,x3)
  andAC(x2,andAC(x3,x4)) -> andAC(andAC(x2,x3),x4)
  andAC(x3,x2) -> andAC(x2,x3)
 TRS:
  not(not(x)) -> x
  orAC(not(x),not(y)) -> not(andAC(x,y))

Proof:
 DP Processor:
  Equations#:
   or{AC,#}(orAC(x2,x3),x4) -> or{AC,#}(x2,orAC(x3,x4))
   or{AC,#}(x2,x3) -> or{AC,#}(x3,x2)
   and{AC,#}(andAC(x2,x3),x4) -> and{AC,#}(x2,andAC(x3,x4))
   and{AC,#}(x2,x3) -> and{AC,#}(x3,x2)
   or{AC,#}(x2,orAC(x3,x4)) -> or{AC,#}(orAC(x2,x3),x4)
   or{AC,#}(x3,x2) -> or{AC,#}(x2,x3)
   and{AC,#}(x2,andAC(x3,x4)) -> and{AC,#}(andAC(x2,x3),x4)
   and{AC,#}(x3,x2) -> and{AC,#}(x2,x3)
  DPs:
   or{AC,#}(not(x),not(y)) -> not#(andAC(x,y))
   or{AC,#}(x5,orAC(not(x),not(y))) -> not#(andAC(x,y))
   or{AC,#}(x5,orAC(not(x),not(y))) -> or{AC,#}(x5,not(andAC(x,y)))
  Equations:
   orAC(orAC(x2,x3),x4) -> orAC(x2,orAC(x3,x4))
   orAC(x2,x3) -> orAC(x3,x2)
   andAC(andAC(x2,x3),x4) -> andAC(x2,andAC(x3,x4))
   andAC(x2,x3) -> andAC(x3,x2)
   orAC(x2,orAC(x3,x4)) -> orAC(orAC(x2,x3),x4)
   orAC(x3,x2) -> orAC(x2,x3)
   andAC(x2,andAC(x3,x4)) -> andAC(andAC(x2,x3),x4)
   andAC(x3,x2) -> andAC(x2,x3)
  TRS:
   not(not(x)) -> x
   orAC(not(x),not(y)) -> not(andAC(x,y))
  S:
   or{AC,#}(orAC(x6,x7),x8) -> or{AC,#}(x6,x7)
   or{AC,#}(x6,orAC(x7,x8)) -> or{AC,#}(x7,x8)
   and{AC,#}(andAC(x6,x7),x8) -> and{AC,#}(x6,x7)
   and{AC,#}(x6,andAC(x7,x8)) -> and{AC,#}(x7,x8)
  AC-EDG Processor:
   Equations#:
    or{AC,#}(orAC(x2,x3),x4) -> or{AC,#}(x2,orAC(x3,x4))
    or{AC,#}(x2,x3) -> or{AC,#}(x3,x2)
    and{AC,#}(andAC(x2,x3),x4) -> and{AC,#}(x2,andAC(x3,x4))
    and{AC,#}(x2,x3) -> and{AC,#}(x3,x2)
    or{AC,#}(x2,orAC(x3,x4)) -> or{AC,#}(orAC(x2,x3),x4)
    or{AC,#}(x3,x2) -> or{AC,#}(x2,x3)
    and{AC,#}(x2,andAC(x3,x4)) -> and{AC,#}(andAC(x2,x3),x4)
    and{AC,#}(x3,x2) -> and{AC,#}(x2,x3)
   DPs:
    or{AC,#}(not(x),not(y)) -> not#(andAC(x,y))
    or{AC,#}(x5,orAC(not(x),not(y))) -> not#(andAC(x,y))
    or{AC,#}(x5,orAC(not(x),not(y))) -> or{AC,#}(x5,not(andAC(x,y)))
   Equations:
    orAC(orAC(x2,x3),x4) -> orAC(x2,orAC(x3,x4))
    orAC(x2,x3) -> orAC(x3,x2)
    andAC(andAC(x2,x3),x4) -> andAC(x2,andAC(x3,x4))
    andAC(x2,x3) -> andAC(x3,x2)
    orAC(x2,orAC(x3,x4)) -> orAC(orAC(x2,x3),x4)
    orAC(x3,x2) -> orAC(x2,x3)
    andAC(x2,andAC(x3,x4)) -> andAC(andAC(x2,x3),x4)
    andAC(x3,x2) -> andAC(x2,x3)
   TRS:
    not(not(x)) -> x
    orAC(not(x),not(y)) -> not(andAC(x,y))
   S:
    or{AC,#}(orAC(x6,x7),x8) -> or{AC,#}(x6,x7)
    or{AC,#}(x6,orAC(x7,x8)) -> or{AC,#}(x7,x8)
    and{AC,#}(andAC(x6,x7),x8) -> and{AC,#}(x6,x7)
    and{AC,#}(x6,andAC(x7,x8)) -> and{AC,#}(x7,x8)
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 3/9
    Equations#:
     or{AC,#}(orAC(x2,x3),x4) -> or{AC,#}(x2,orAC(x3,x4))
     or{AC,#}(x2,x3) -> or{AC,#}(x3,x2)
     and{AC,#}(andAC(x2,x3),x4) -> and{AC,#}(x2,andAC(x3,x4))
     and{AC,#}(x2,x3) -> and{AC,#}(x3,x2)
     or{AC,#}(x2,orAC(x3,x4)) -> or{AC,#}(orAC(x2,x3),x4)
     or{AC,#}(x3,x2) -> or{AC,#}(x2,x3)
     and{AC,#}(x2,andAC(x3,x4)) -> and{AC,#}(andAC(x2,x3),x4)
     and{AC,#}(x3,x2) -> and{AC,#}(x2,x3)
    DPs:
     or{AC,#}(x5,orAC(not(x),not(y))) -> or{AC,#}(x5,not(andAC(x,y)))
    Equations:
     orAC(orAC(x2,x3),x4) -> orAC(x2,orAC(x3,x4))
     orAC(x2,x3) -> orAC(x3,x2)
     andAC(andAC(x2,x3),x4) -> andAC(x2,andAC(x3,x4))
     andAC(x2,x3) -> andAC(x3,x2)
     orAC(x2,orAC(x3,x4)) -> orAC(orAC(x2,x3),x4)
     orAC(x3,x2) -> orAC(x2,x3)
     andAC(x2,andAC(x3,x4)) -> andAC(andAC(x2,x3),x4)
     andAC(x3,x2) -> andAC(x2,x3)
    TRS:
     not(not(x)) -> x
     orAC(not(x),not(y)) -> not(andAC(x,y))
    S:
     or{AC,#}(orAC(x6,x7),x8) -> or{AC,#}(x6,x7)
     or{AC,#}(x6,orAC(x7,x8)) -> or{AC,#}(x7,x8)
     and{AC,#}(andAC(x6,x7),x8) -> and{AC,#}(x6,x7)
     and{AC,#}(x6,andAC(x7,x8)) -> and{AC,#}(x7,x8)
    AC-DP unlabeling:
     Equations#:
      orAC(orAC(x2,x3),x4) -> orAC(x2,orAC(x3,x4))
      orAC(x2,x3) -> orAC(x3,x2)
      andAC(andAC(x2,x3),x4) -> andAC(x2,andAC(x3,x4))
      andAC(x2,x3) -> andAC(x3,x2)
      orAC(x2,orAC(x3,x4)) -> orAC(orAC(x2,x3),x4)
      orAC(x3,x2) -> orAC(x2,x3)
      andAC(x2,andAC(x3,x4)) -> andAC(andAC(x2,x3),x4)
      andAC(x3,x2) -> andAC(x2,x3)
     DPs:
      orAC(x5,orAC(not(x),not(y))) -> orAC(x5,not(andAC(x,y)))
     Equations:
      orAC(orAC(x2,x3),x4) -> orAC(x2,orAC(x3,x4))
      orAC(x2,x3) -> orAC(x3,x2)
      andAC(andAC(x2,x3),x4) -> andAC(x2,andAC(x3,x4))
      andAC(x2,x3) -> andAC(x3,x2)
      orAC(x2,orAC(x3,x4)) -> orAC(orAC(x2,x3),x4)
      orAC(x3,x2) -> orAC(x2,x3)
      andAC(x2,andAC(x3,x4)) -> andAC(andAC(x2,x3),x4)
      andAC(x3,x2) -> andAC(x2,x3)
     TRS:
      not(not(x)) -> x
      orAC(not(x),not(y)) -> not(andAC(x,y))
     S:
      orAC(orAC(x6,x7),x8) -> orAC(x6,x7)
      orAC(x6,orAC(x7,x8)) -> orAC(x7,x8)
      andAC(andAC(x6,x7),x8) -> andAC(x6,x7)
      andAC(x6,andAC(x7,x8)) -> andAC(x7,x8)
     Usable Rule Processor:
      Equations#:
       orAC(orAC(x2,x3),x4) -> orAC(x2,orAC(x3,x4))
       orAC(x2,x3) -> orAC(x3,x2)
       andAC(andAC(x2,x3),x4) -> andAC(x2,andAC(x3,x4))
       andAC(x2,x3) -> andAC(x3,x2)
       orAC(x2,orAC(x3,x4)) -> orAC(orAC(x2,x3),x4)
       orAC(x3,x2) -> orAC(x2,x3)
       andAC(x2,andAC(x3,x4)) -> andAC(andAC(x2,x3),x4)
       andAC(x3,x2) -> andAC(x2,x3)
      DPs:
       orAC(x5,orAC(not(x),not(y))) -> orAC(x5,not(andAC(x,y)))
      Equations:
       orAC(orAC(x2,x3),x4) -> orAC(x2,orAC(x3,x4))
       orAC(x2,x3) -> orAC(x3,x2)
       andAC(andAC(x2,x3),x4) -> andAC(x2,andAC(x3,x4))
       andAC(x2,x3) -> andAC(x3,x2)
       orAC(x2,orAC(x3,x4)) -> orAC(orAC(x2,x3),x4)
       orAC(x3,x2) -> orAC(x2,x3)
       andAC(x2,andAC(x3,x4)) -> andAC(andAC(x2,x3),x4)
       andAC(x3,x2) -> andAC(x2,x3)
      TRS:
       orAC(not(x),not(y)) -> not(andAC(x,y))
      S:
       orAC(orAC(x6,x7),x8) -> orAC(x6,x7)
       orAC(x6,orAC(x7,x8)) -> orAC(x7,x8)
       andAC(andAC(x6,x7),x8) -> andAC(x6,x7)
       andAC(x6,andAC(x7,x8)) -> andAC(x7,x8)
      AC-KBO Processor:
       argument filtering:
        pi(orAC) = [0,1]
        pi(andAC) = [0,1]
        pi(not) = 0
       precedence:
        not ~ orAC > andAC
        weight function:
         [not](x0) = x0,
         
         [andAC](x0, x1) = x0 + x1,
         
         [orAC](x0, x1) = x0 + x1 + 1
         usable rules:
          orAC(not(x),not(y)) -> not(andAC(x,y))
         problem:
          Equations#:
           orAC(orAC(x2,x3),x4) -> orAC(x2,orAC(x3,x4))
           orAC(x2,x3) -> orAC(x3,x2)
           andAC(andAC(x2,x3),x4) -> andAC(x2,andAC(x3,x4))
           andAC(x2,x3) -> andAC(x3,x2)
           orAC(x2,orAC(x3,x4)) -> orAC(orAC(x2,x3),x4)
           orAC(x3,x2) -> orAC(x2,x3)
           andAC(x2,andAC(x3,x4)) -> andAC(andAC(x2,x3),x4)
           andAC(x3,x2) -> andAC(x2,x3)
          DPs:
           
          Equations:
           orAC(orAC(x2,x3),x4) -> orAC(x2,orAC(x3,x4))
           orAC(x2,x3) -> orAC(x3,x2)
           andAC(andAC(x2,x3),x4) -> andAC(x2,andAC(x3,x4))
           andAC(x2,x3) -> andAC(x3,x2)
           orAC(x2,orAC(x3,x4)) -> orAC(orAC(x2,x3),x4)
           orAC(x3,x2) -> orAC(x2,x3)
           andAC(x2,andAC(x3,x4)) -> andAC(andAC(x2,x3),x4)
           andAC(x3,x2) -> andAC(x2,x3)
          TRS:
           orAC(not(x),not(y)) -> not(andAC(x,y))
          S:
           orAC(orAC(x6,x7),x8) -> orAC(x6,x7)
           orAC(x6,orAC(x7,x8)) -> orAC(x7,x8)
           andAC(andAC(x6,x7),x8) -> andAC(x6,x7)
           andAC(x6,andAC(x7,x8)) -> andAC(x7,x8)
         Qed