YES
Time: 0.072

Problem:
 Equations:
  joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
  joinAC(x2,x3) -> joinAC(x3,x2)
  meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
  meetAC(x2,x3) -> meetAC(x3,x2)
  joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
  joinAC(x3,x2) -> joinAC(x2,x3)
  meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
  meetAC(x3,x2) -> meetAC(x2,x3)
 TRS:
  joinAC(x,meetAC(x,y)) -> x
  meetAC(x,joinAC(x,y)) -> x

Proof:
 DP Processor:
  Equations#:
   join{AC,#}(joinAC(x2,x3),x4) -> join{AC,#}(x2,joinAC(x3,x4))
   join{AC,#}(x2,x3) -> join{AC,#}(x3,x2)
   meet{AC,#}(meetAC(x2,x3),x4) -> meet{AC,#}(x2,meetAC(x3,x4))
   meet{AC,#}(x2,x3) -> meet{AC,#}(x3,x2)
   join{AC,#}(x2,joinAC(x3,x4)) -> join{AC,#}(joinAC(x2,x3),x4)
   join{AC,#}(x3,x2) -> join{AC,#}(x2,x3)
   meet{AC,#}(x2,meetAC(x3,x4)) -> meet{AC,#}(meetAC(x2,x3),x4)
   meet{AC,#}(x3,x2) -> meet{AC,#}(x2,x3)
  DPs:
   join{AC,#}(x5,joinAC(x,meetAC(x,y))) -> join{AC,#}(x5,x)
   meet{AC,#}(x6,meetAC(x,joinAC(x,y))) -> meet{AC,#}(x6,x)
  Equations:
   joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
   joinAC(x2,x3) -> joinAC(x3,x2)
   meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
   meetAC(x2,x3) -> meetAC(x3,x2)
   joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
   joinAC(x3,x2) -> joinAC(x2,x3)
   meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
   meetAC(x3,x2) -> meetAC(x2,x3)
  TRS:
   joinAC(x,meetAC(x,y)) -> x
   meetAC(x,joinAC(x,y)) -> x
  S:
   join{AC,#}(joinAC(x7,x8),x9) -> join{AC,#}(x7,x8)
   join{AC,#}(x7,joinAC(x8,x9)) -> join{AC,#}(x8,x9)
   meet{AC,#}(meetAC(x7,x8),x9) -> meet{AC,#}(x7,x8)
   meet{AC,#}(x7,meetAC(x8,x9)) -> meet{AC,#}(x8,x9)
  AC-EDG Processor:
   Equations#:
    join{AC,#}(joinAC(x2,x3),x4) -> join{AC,#}(x2,joinAC(x3,x4))
    join{AC,#}(x2,x3) -> join{AC,#}(x3,x2)
    meet{AC,#}(meetAC(x2,x3),x4) -> meet{AC,#}(x2,meetAC(x3,x4))
    meet{AC,#}(x2,x3) -> meet{AC,#}(x3,x2)
    join{AC,#}(x2,joinAC(x3,x4)) -> join{AC,#}(joinAC(x2,x3),x4)
    join{AC,#}(x3,x2) -> join{AC,#}(x2,x3)
    meet{AC,#}(x2,meetAC(x3,x4)) -> meet{AC,#}(meetAC(x2,x3),x4)
    meet{AC,#}(x3,x2) -> meet{AC,#}(x2,x3)
   DPs:
    join{AC,#}(x5,joinAC(x,meetAC(x,y))) -> join{AC,#}(x5,x)
    meet{AC,#}(x6,meetAC(x,joinAC(x,y))) -> meet{AC,#}(x6,x)
   Equations:
    joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
    joinAC(x2,x3) -> joinAC(x3,x2)
    meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
    meetAC(x2,x3) -> meetAC(x3,x2)
    joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
    joinAC(x3,x2) -> joinAC(x2,x3)
    meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
    meetAC(x3,x2) -> meetAC(x2,x3)
   TRS:
    joinAC(x,meetAC(x,y)) -> x
    meetAC(x,joinAC(x,y)) -> x
   S:
    join{AC,#}(joinAC(x7,x8),x9) -> join{AC,#}(x7,x8)
    join{AC,#}(x7,joinAC(x8,x9)) -> join{AC,#}(x8,x9)
    meet{AC,#}(meetAC(x7,x8),x9) -> meet{AC,#}(x7,x8)
    meet{AC,#}(x7,meetAC(x8,x9)) -> meet{AC,#}(x8,x9)
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 2/4
    Equations#:
     join{AC,#}(joinAC(x2,x3),x4) -> join{AC,#}(x2,joinAC(x3,x4))
     join{AC,#}(x2,x3) -> join{AC,#}(x3,x2)
     meet{AC,#}(meetAC(x2,x3),x4) -> meet{AC,#}(x2,meetAC(x3,x4))
     meet{AC,#}(x2,x3) -> meet{AC,#}(x3,x2)
     join{AC,#}(x2,joinAC(x3,x4)) -> join{AC,#}(joinAC(x2,x3),x4)
     join{AC,#}(x3,x2) -> join{AC,#}(x2,x3)
     meet{AC,#}(x2,meetAC(x3,x4)) -> meet{AC,#}(meetAC(x2,x3),x4)
     meet{AC,#}(x3,x2) -> meet{AC,#}(x2,x3)
    DPs:
     join{AC,#}(x5,joinAC(x,meetAC(x,y))) -> join{AC,#}(x5,x)
    Equations:
     joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
     joinAC(x2,x3) -> joinAC(x3,x2)
     meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
     meetAC(x2,x3) -> meetAC(x3,x2)
     joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
     joinAC(x3,x2) -> joinAC(x2,x3)
     meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
     meetAC(x3,x2) -> meetAC(x2,x3)
    TRS:
     joinAC(x,meetAC(x,y)) -> x
     meetAC(x,joinAC(x,y)) -> x
    S:
     join{AC,#}(joinAC(x7,x8),x9) -> join{AC,#}(x7,x8)
     join{AC,#}(x7,joinAC(x8,x9)) -> join{AC,#}(x8,x9)
     meet{AC,#}(meetAC(x7,x8),x9) -> meet{AC,#}(x7,x8)
     meet{AC,#}(x7,meetAC(x8,x9)) -> meet{AC,#}(x8,x9)
    AC-DP unlabeling:
     Equations#:
      joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
      joinAC(x2,x3) -> joinAC(x3,x2)
      meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
      meetAC(x2,x3) -> meetAC(x3,x2)
      joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
      joinAC(x3,x2) -> joinAC(x2,x3)
      meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
      meetAC(x3,x2) -> meetAC(x2,x3)
     DPs:
      joinAC(x5,joinAC(x,meetAC(x,y))) -> joinAC(x5,x)
     Equations:
      joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
      joinAC(x2,x3) -> joinAC(x3,x2)
      meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
      meetAC(x2,x3) -> meetAC(x3,x2)
      joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
      joinAC(x3,x2) -> joinAC(x2,x3)
      meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
      meetAC(x3,x2) -> meetAC(x2,x3)
     TRS:
      joinAC(x,meetAC(x,y)) -> x
      meetAC(x,joinAC(x,y)) -> x
     S:
      joinAC(joinAC(x7,x8),x9) -> joinAC(x7,x8)
      joinAC(x7,joinAC(x8,x9)) -> joinAC(x8,x9)
      meetAC(meetAC(x7,x8),x9) -> meetAC(x7,x8)
      meetAC(x7,meetAC(x8,x9)) -> meetAC(x8,x9)
     Usable Rule Processor:
      Equations#:
       joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
       joinAC(x2,x3) -> joinAC(x3,x2)
       meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
       meetAC(x2,x3) -> meetAC(x3,x2)
       joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
       joinAC(x3,x2) -> joinAC(x2,x3)
       meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
       meetAC(x3,x2) -> meetAC(x2,x3)
      DPs:
       joinAC(x5,joinAC(x,meetAC(x,y))) -> joinAC(x5,x)
      Equations:
       joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
       joinAC(x2,x3) -> joinAC(x3,x2)
       meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
       meetAC(x2,x3) -> meetAC(x3,x2)
       joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
       joinAC(x3,x2) -> joinAC(x2,x3)
       meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
       meetAC(x3,x2) -> meetAC(x2,x3)
      TRS:
       joinAC(x,meetAC(x,y)) -> x
      S:
       joinAC(joinAC(x7,x8),x9) -> joinAC(x7,x8)
       joinAC(x7,joinAC(x8,x9)) -> joinAC(x8,x9)
       meetAC(meetAC(x7,x8),x9) -> meetAC(x7,x8)
       meetAC(x7,meetAC(x8,x9)) -> meetAC(x8,x9)
      AC-KBO Processor:
       argument filtering:
        pi(joinAC) = [0,1]
        pi(meetAC) = [0,1]
       precedence:
        meetAC ~ joinAC
        weight function:
         w0 = 1
         w(joinAC) = 4
         w(meetAC) = 0
         usable rules:
          joinAC(x,meetAC(x,y)) -> x
         problem:
          Equations#:
           joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
           joinAC(x2,x3) -> joinAC(x3,x2)
           meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
           meetAC(x2,x3) -> meetAC(x3,x2)
           joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
           joinAC(x3,x2) -> joinAC(x2,x3)
           meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
           meetAC(x3,x2) -> meetAC(x2,x3)
          DPs:
           
          Equations:
           joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
           joinAC(x2,x3) -> joinAC(x3,x2)
           meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
           meetAC(x2,x3) -> meetAC(x3,x2)
           joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
           joinAC(x3,x2) -> joinAC(x2,x3)
           meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
           meetAC(x3,x2) -> meetAC(x2,x3)
          TRS:
           joinAC(x,meetAC(x,y)) -> x
          S:
           joinAC(joinAC(x7,x8),x9) -> joinAC(x7,x8)
           joinAC(x7,joinAC(x8,x9)) -> joinAC(x8,x9)
           meetAC(meetAC(x7,x8),x9) -> meetAC(x7,x8)
           meetAC(x7,meetAC(x8,x9)) -> meetAC(x8,x9)
         Qed
     
     Equations#:
      join{AC,#}(joinAC(x2,x3),x4) -> join{AC,#}(x2,joinAC(x3,x4))
      join{AC,#}(x2,x3) -> join{AC,#}(x3,x2)
      meet{AC,#}(meetAC(x2,x3),x4) -> meet{AC,#}(x2,meetAC(x3,x4))
      meet{AC,#}(x2,x3) -> meet{AC,#}(x3,x2)
      join{AC,#}(x2,joinAC(x3,x4)) -> join{AC,#}(joinAC(x2,x3),x4)
      join{AC,#}(x3,x2) -> join{AC,#}(x2,x3)
      meet{AC,#}(x2,meetAC(x3,x4)) -> meet{AC,#}(meetAC(x2,x3),x4)
      meet{AC,#}(x3,x2) -> meet{AC,#}(x2,x3)
     DPs:
      meet{AC,#}(x6,meetAC(x,joinAC(x,y))) -> meet{AC,#}(x6,x)
     Equations:
      joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
      joinAC(x2,x3) -> joinAC(x3,x2)
      meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
      meetAC(x2,x3) -> meetAC(x3,x2)
      joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
      joinAC(x3,x2) -> joinAC(x2,x3)
      meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
      meetAC(x3,x2) -> meetAC(x2,x3)
     TRS:
      joinAC(x,meetAC(x,y)) -> x
      meetAC(x,joinAC(x,y)) -> x
     S:
      join{AC,#}(joinAC(x7,x8),x9) -> join{AC,#}(x7,x8)
      join{AC,#}(x7,joinAC(x8,x9)) -> join{AC,#}(x8,x9)
      meet{AC,#}(meetAC(x7,x8),x9) -> meet{AC,#}(x7,x8)
      meet{AC,#}(x7,meetAC(x8,x9)) -> meet{AC,#}(x8,x9)
     AC-DP unlabeling:
      Equations#:
       joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
       joinAC(x2,x3) -> joinAC(x3,x2)
       meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
       meetAC(x2,x3) -> meetAC(x3,x2)
       joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
       joinAC(x3,x2) -> joinAC(x2,x3)
       meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
       meetAC(x3,x2) -> meetAC(x2,x3)
      DPs:
       meetAC(x6,meetAC(x,joinAC(x,y))) -> meetAC(x6,x)
      Equations:
       joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
       joinAC(x2,x3) -> joinAC(x3,x2)
       meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
       meetAC(x2,x3) -> meetAC(x3,x2)
       joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
       joinAC(x3,x2) -> joinAC(x2,x3)
       meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
       meetAC(x3,x2) -> meetAC(x2,x3)
      TRS:
       joinAC(x,meetAC(x,y)) -> x
       meetAC(x,joinAC(x,y)) -> x
      S:
       joinAC(joinAC(x7,x8),x9) -> joinAC(x7,x8)
       joinAC(x7,joinAC(x8,x9)) -> joinAC(x8,x9)
       meetAC(meetAC(x7,x8),x9) -> meetAC(x7,x8)
       meetAC(x7,meetAC(x8,x9)) -> meetAC(x8,x9)
      Usable Rule Processor:
       Equations#:
        joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
        joinAC(x2,x3) -> joinAC(x3,x2)
        meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
        meetAC(x2,x3) -> meetAC(x3,x2)
        joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
        joinAC(x3,x2) -> joinAC(x2,x3)
        meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
        meetAC(x3,x2) -> meetAC(x2,x3)
       DPs:
        meetAC(x6,meetAC(x,joinAC(x,y))) -> meetAC(x6,x)
       Equations:
        joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
        joinAC(x2,x3) -> joinAC(x3,x2)
        meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
        meetAC(x2,x3) -> meetAC(x3,x2)
        joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
        joinAC(x3,x2) -> joinAC(x2,x3)
        meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
        meetAC(x3,x2) -> meetAC(x2,x3)
       TRS:
        meetAC(x,joinAC(x,y)) -> x
       S:
        joinAC(joinAC(x7,x8),x9) -> joinAC(x7,x8)
        joinAC(x7,joinAC(x8,x9)) -> joinAC(x8,x9)
        meetAC(meetAC(x7,x8),x9) -> meetAC(x7,x8)
        meetAC(x7,meetAC(x8,x9)) -> meetAC(x8,x9)
       AC-KBO Processor:
        argument filtering:
         pi(joinAC) = [0,1]
         pi(meetAC) = [0,1]
        precedence:
         meetAC ~ joinAC
         weight function:
          w0 = 1
          w(meetAC) = 3
          w(joinAC) = 0
          usable rules:
           meetAC(x,joinAC(x,y)) -> x
          problem:
           Equations#:
            joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
            joinAC(x2,x3) -> joinAC(x3,x2)
            meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
            meetAC(x2,x3) -> meetAC(x3,x2)
            joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
            joinAC(x3,x2) -> joinAC(x2,x3)
            meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
            meetAC(x3,x2) -> meetAC(x2,x3)
           DPs:
            
           Equations:
            joinAC(joinAC(x2,x3),x4) -> joinAC(x2,joinAC(x3,x4))
            joinAC(x2,x3) -> joinAC(x3,x2)
            meetAC(meetAC(x2,x3),x4) -> meetAC(x2,meetAC(x3,x4))
            meetAC(x2,x3) -> meetAC(x3,x2)
            joinAC(x2,joinAC(x3,x4)) -> joinAC(joinAC(x2,x3),x4)
            joinAC(x3,x2) -> joinAC(x2,x3)
            meetAC(x2,meetAC(x3,x4)) -> meetAC(meetAC(x2,x3),x4)
            meetAC(x3,x2) -> meetAC(x2,x3)
           TRS:
            meetAC(x,joinAC(x,y)) -> x
           S:
            joinAC(joinAC(x7,x8),x9) -> joinAC(x7,x8)
            joinAC(x7,joinAC(x8,x9)) -> joinAC(x8,x9)
            meetAC(meetAC(x7,x8),x9) -> meetAC(x7,x8)
            meetAC(x7,meetAC(x8,x9)) -> meetAC(x8,x9)
          Qed