YES
Time: 0.075

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:
  andAC(x,0()) -> 0()
  andAC(x,1()) -> x
  andAC(x,x) -> x
  orAC(x,0()) -> x
  orAC(x,1()) -> 1()
  orAC(x,x) -> 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:
   and{AC,#}(x6,andAC(x,0())) -> and{AC,#}(x6,0())
   and{AC,#}(x7,andAC(x,1())) -> and{AC,#}(x7,x)
   and{AC,#}(x8,andAC(x,x)) -> and{AC,#}(x8,x)
   or{AC,#}(x9,orAC(x,0())) -> or{AC,#}(x9,x)
   or{AC,#}(x10,orAC(x,1())) -> or{AC,#}(x10,1())
   or{AC,#}(x11,orAC(x,x)) -> or{AC,#}(x11,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,0()) -> 0()
   andAC(x,1()) -> x
   andAC(x,x) -> x
   orAC(x,0()) -> x
   orAC(x,1()) -> 1()
   orAC(x,x) -> x
  S:
   and{AC,#}(andAC(x12,x13),x14) -> and{AC,#}(x12,x13)
   and{AC,#}(x12,andAC(x13,x14)) -> and{AC,#}(x13,x14)
   or{AC,#}(orAC(x12,x13),x14) -> or{AC,#}(x12,x13)
   or{AC,#}(x12,orAC(x13,x14)) -> or{AC,#}(x13,x14)
  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:
    and{AC,#}(x6,andAC(x,0())) -> and{AC,#}(x6,0())
    and{AC,#}(x7,andAC(x,1())) -> and{AC,#}(x7,x)
    and{AC,#}(x8,andAC(x,x)) -> and{AC,#}(x8,x)
    or{AC,#}(x9,orAC(x,0())) -> or{AC,#}(x9,x)
    or{AC,#}(x10,orAC(x,1())) -> or{AC,#}(x10,1())
    or{AC,#}(x11,orAC(x,x)) -> or{AC,#}(x11,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,0()) -> 0()
    andAC(x,1()) -> x
    andAC(x,x) -> x
    orAC(x,0()) -> x
    orAC(x,1()) -> 1()
    orAC(x,x) -> x
   S:
    and{AC,#}(andAC(x12,x13),x14) -> and{AC,#}(x12,x13)
    and{AC,#}(x12,andAC(x13,x14)) -> and{AC,#}(x13,x14)
    or{AC,#}(orAC(x12,x13),x14) -> or{AC,#}(x12,x13)
    or{AC,#}(x12,orAC(x13,x14)) -> or{AC,#}(x13,x14)
   SCC Processor:
    #sccs: 2
    #rules: 6
    #arcs: 18/36
    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,#}(x8,andAC(x,x)) -> and{AC,#}(x8,x)
     and{AC,#}(x7,andAC(x,1())) -> and{AC,#}(x7,x)
     and{AC,#}(x6,andAC(x,0())) -> and{AC,#}(x6,0())
    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,0()) -> 0()
     andAC(x,1()) -> x
     andAC(x,x) -> x
     orAC(x,0()) -> x
     orAC(x,1()) -> 1()
     orAC(x,x) -> x
    S:
     and{AC,#}(andAC(x12,x13),x14) -> and{AC,#}(x12,x13)
     and{AC,#}(x12,andAC(x13,x14)) -> and{AC,#}(x13,x14)
     or{AC,#}(orAC(x12,x13),x14) -> or{AC,#}(x12,x13)
     or{AC,#}(x12,orAC(x13,x14)) -> or{AC,#}(x13,x14)
    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(x8,andAC(x,x)) -> andAC(x8,x)
      andAC(x7,andAC(x,1())) -> andAC(x7,x)
      andAC(x6,andAC(x,0())) -> andAC(x6,0())
     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,0()) -> 0()
      andAC(x,1()) -> x
      andAC(x,x) -> x
      orAC(x,0()) -> x
      orAC(x,1()) -> 1()
      orAC(x,x) -> x
     S:
      andAC(andAC(x12,x13),x14) -> andAC(x12,x13)
      andAC(x12,andAC(x13,x14)) -> andAC(x13,x14)
      orAC(orAC(x12,x13),x14) -> orAC(x12,x13)
      orAC(x12,orAC(x13,x14)) -> orAC(x13,x14)
     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(x8,andAC(x,x)) -> andAC(x8,x)
       andAC(x7,andAC(x,1())) -> andAC(x7,x)
       andAC(x6,andAC(x,0())) -> andAC(x6,0())
      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,0()) -> 0()
       andAC(x,1()) -> x
       andAC(x,x) -> x
      S:
       andAC(andAC(x12,x13),x14) -> andAC(x12,x13)
       andAC(x12,andAC(x13,x14)) -> andAC(x13,x14)
       orAC(orAC(x12,x13),x14) -> orAC(x12,x13)
       orAC(x12,orAC(x13,x14)) -> orAC(x13,x14)
      AC-KBO Processor:
       argument filtering:
        pi(andAC) = [0,1]
        pi(0) = []
        pi(1) = []
       precedence:
        1 ~ 0 ~ andAC
        weight function:
         w0 = 1
         w(andAC) = 4
         w(1) = w(0) = 1
         usable rules:
          andAC(x,0()) -> 0()
          andAC(x,1()) -> x
          andAC(x,x) -> x
         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,0()) -> 0()
           andAC(x,1()) -> x
           andAC(x,x) -> x
          S:
           andAC(andAC(x12,x13),x14) -> andAC(x12,x13)
           andAC(x12,andAC(x13,x14)) -> andAC(x13,x14)
           orAC(orAC(x12,x13),x14) -> orAC(x12,x13)
           orAC(x12,orAC(x13,x14)) -> orAC(x13,x14)
         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,#}(x11,orAC(x,x)) -> or{AC,#}(x11,x)
      or{AC,#}(x10,orAC(x,1())) -> or{AC,#}(x10,1())
      or{AC,#}(x9,orAC(x,0())) -> or{AC,#}(x9,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,0()) -> 0()
      andAC(x,1()) -> x
      andAC(x,x) -> x
      orAC(x,0()) -> x
      orAC(x,1()) -> 1()
      orAC(x,x) -> x
     S:
      and{AC,#}(andAC(x12,x13),x14) -> and{AC,#}(x12,x13)
      and{AC,#}(x12,andAC(x13,x14)) -> and{AC,#}(x13,x14)
      or{AC,#}(orAC(x12,x13),x14) -> or{AC,#}(x12,x13)
      or{AC,#}(x12,orAC(x13,x14)) -> or{AC,#}(x13,x14)
     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(x11,orAC(x,x)) -> orAC(x11,x)
       orAC(x10,orAC(x,1())) -> orAC(x10,1())
       orAC(x9,orAC(x,0())) -> orAC(x9,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,0()) -> 0()
       andAC(x,1()) -> x
       andAC(x,x) -> x
       orAC(x,0()) -> x
       orAC(x,1()) -> 1()
       orAC(x,x) -> x
      S:
       andAC(andAC(x12,x13),x14) -> andAC(x12,x13)
       andAC(x12,andAC(x13,x14)) -> andAC(x13,x14)
       orAC(orAC(x12,x13),x14) -> orAC(x12,x13)
       orAC(x12,orAC(x13,x14)) -> orAC(x13,x14)
      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(x11,orAC(x,x)) -> orAC(x11,x)
        orAC(x10,orAC(x,1())) -> orAC(x10,1())
        orAC(x9,orAC(x,0())) -> orAC(x9,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:
        orAC(x,0()) -> x
        orAC(x,1()) -> 1()
        orAC(x,x) -> x
       S:
        andAC(andAC(x12,x13),x14) -> andAC(x12,x13)
        andAC(x12,andAC(x13,x14)) -> andAC(x13,x14)
        orAC(orAC(x12,x13),x14) -> orAC(x12,x13)
        orAC(x12,orAC(x13,x14)) -> orAC(x13,x14)
       AC-KBO Processor:
        argument filtering:
         pi(orAC) = [0,1]
         pi(0) = []
         pi(1) = []
        precedence:
         1 ~ 0 ~ orAC
         weight function:
          w0 = 1
          w(orAC) = 4
          w(0) = 2
          w(1) = 1
          usable rules:
           orAC(x,0()) -> x
           orAC(x,1()) -> 1()
           orAC(x,x) -> x
          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(x,0()) -> x
            orAC(x,1()) -> 1()
            orAC(x,x) -> x
           S:
            andAC(andAC(x12,x13),x14) -> andAC(x12,x13)
            andAC(x12,andAC(x13,x14)) -> andAC(x13,x14)
            orAC(orAC(x12,x13),x14) -> orAC(x12,x13)
            orAC(x12,orAC(x13,x14)) -> orAC(x13,x14)
          Qed