YES
Time: 0.169

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

Proof:
 DP Processor:
  Equations#:
   join{AC,#}(joinAC(x3,x4),x5) -> join{AC,#}(x3,joinAC(x4,x5))
   join{AC,#}(x3,x4) -> join{AC,#}(x4,x3)
   meet{AC,#}(meetAC(x3,x4),x5) -> meet{AC,#}(x3,meetAC(x4,x5))
   meet{AC,#}(x3,x4) -> meet{AC,#}(x4,x3)
   join{AC,#}(x3,joinAC(x4,x5)) -> join{AC,#}(joinAC(x3,x4),x5)
   join{AC,#}(x4,x3) -> join{AC,#}(x3,x4)
   meet{AC,#}(x3,meetAC(x4,x5)) -> meet{AC,#}(meetAC(x3,x4),x5)
   meet{AC,#}(x4,x3) -> meet{AC,#}(x3,x4)
  DPs:
   join{AC,#}(x,meetAC(y,z)) -> join{AC,#}(x,z)
   join{AC,#}(x,meetAC(y,z)) -> join{AC,#}(x,y)
   join{AC,#}(x,meetAC(y,z)) -> meet{AC,#}(joinAC(x,y),joinAC(x,z))
   join{AC,#}(x6,joinAC(x,meetAC(x,y))) -> join{AC,#}(x6,x)
   meet{AC,#}(x7,meetAC(x,joinAC(x,y))) -> meet{AC,#}(x7,x)
   join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x,z)
   join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x,y)
   join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> meet{AC,#}(joinAC(x,y),joinAC(x,z))
   join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x8,meetAC(joinAC(x,y),joinAC(x,z)))
  Equations:
   joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
   joinAC(x3,x4) -> joinAC(x4,x3)
   meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
   meetAC(x3,x4) -> meetAC(x4,x3)
   joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
   joinAC(x4,x3) -> joinAC(x3,x4)
   meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
   meetAC(x4,x3) -> meetAC(x3,x4)
  TRS:
   joinAC(x,meetAC(x,y)) -> x
   meetAC(x,joinAC(x,y)) -> x
   joinAC(x,meetAC(y,z)) -> meetAC(joinAC(x,y),joinAC(x,z))
  S:
   join{AC,#}(joinAC(x9,x10),x11) -> join{AC,#}(x9,x10)
   join{AC,#}(x9,joinAC(x10,x11)) -> join{AC,#}(x10,x11)
   meet{AC,#}(meetAC(x9,x10),x11) -> meet{AC,#}(x9,x10)
   meet{AC,#}(x9,meetAC(x10,x11)) -> meet{AC,#}(x10,x11)
  AC-EDG Processor:
   Equations#:
    join{AC,#}(joinAC(x3,x4),x5) -> join{AC,#}(x3,joinAC(x4,x5))
    join{AC,#}(x3,x4) -> join{AC,#}(x4,x3)
    meet{AC,#}(meetAC(x3,x4),x5) -> meet{AC,#}(x3,meetAC(x4,x5))
    meet{AC,#}(x3,x4) -> meet{AC,#}(x4,x3)
    join{AC,#}(x3,joinAC(x4,x5)) -> join{AC,#}(joinAC(x3,x4),x5)
    join{AC,#}(x4,x3) -> join{AC,#}(x3,x4)
    meet{AC,#}(x3,meetAC(x4,x5)) -> meet{AC,#}(meetAC(x3,x4),x5)
    meet{AC,#}(x4,x3) -> meet{AC,#}(x3,x4)
   DPs:
    join{AC,#}(x,meetAC(y,z)) -> join{AC,#}(x,z)
    join{AC,#}(x,meetAC(y,z)) -> join{AC,#}(x,y)
    join{AC,#}(x,meetAC(y,z)) -> meet{AC,#}(joinAC(x,y),joinAC(x,z))
    join{AC,#}(x6,joinAC(x,meetAC(x,y))) -> join{AC,#}(x6,x)
    meet{AC,#}(x7,meetAC(x,joinAC(x,y))) -> meet{AC,#}(x7,x)
    join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x,z)
    join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x,y)
    join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> meet{AC,#}(joinAC(x,y),joinAC(x,z))
    join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x8,meetAC(joinAC(x,y),joinAC(x,z)))
   Equations:
    joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
    joinAC(x3,x4) -> joinAC(x4,x3)
    meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
    meetAC(x3,x4) -> meetAC(x4,x3)
    joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
    joinAC(x4,x3) -> joinAC(x3,x4)
    meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
    meetAC(x4,x3) -> meetAC(x3,x4)
   TRS:
    joinAC(x,meetAC(x,y)) -> x
    meetAC(x,joinAC(x,y)) -> x
    joinAC(x,meetAC(y,z)) -> meetAC(joinAC(x,y),joinAC(x,z))
   S:
    join{AC,#}(joinAC(x9,x10),x11) -> join{AC,#}(x9,x10)
    join{AC,#}(x9,joinAC(x10,x11)) -> join{AC,#}(x10,x11)
    meet{AC,#}(meetAC(x9,x10),x11) -> meet{AC,#}(x9,x10)
    meet{AC,#}(x9,meetAC(x10,x11)) -> meet{AC,#}(x10,x11)
   SCC Processor:
    #sccs: 2
    #rules: 7
    #arcs: 51/81
    Equations#:
     join{AC,#}(joinAC(x3,x4),x5) -> join{AC,#}(x3,joinAC(x4,x5))
     join{AC,#}(x3,x4) -> join{AC,#}(x4,x3)
     meet{AC,#}(meetAC(x3,x4),x5) -> meet{AC,#}(x3,meetAC(x4,x5))
     meet{AC,#}(x3,x4) -> meet{AC,#}(x4,x3)
     join{AC,#}(x3,joinAC(x4,x5)) -> join{AC,#}(joinAC(x3,x4),x5)
     join{AC,#}(x4,x3) -> join{AC,#}(x3,x4)
     meet{AC,#}(x3,meetAC(x4,x5)) -> meet{AC,#}(meetAC(x3,x4),x5)
     meet{AC,#}(x4,x3) -> meet{AC,#}(x3,x4)
    DPs:
     join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x8,meetAC(joinAC(x,y),joinAC(x,z)))
     join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x,y)
     join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x,z)
     join{AC,#}(x6,joinAC(x,meetAC(x,y))) -> join{AC,#}(x6,x)
     join{AC,#}(x,meetAC(y,z)) -> join{AC,#}(x,y)
     join{AC,#}(x,meetAC(y,z)) -> join{AC,#}(x,z)
    Equations:
     joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
     joinAC(x3,x4) -> joinAC(x4,x3)
     meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
     meetAC(x3,x4) -> meetAC(x4,x3)
     joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
     joinAC(x4,x3) -> joinAC(x3,x4)
     meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
     meetAC(x4,x3) -> meetAC(x3,x4)
    TRS:
     joinAC(x,meetAC(x,y)) -> x
     meetAC(x,joinAC(x,y)) -> x
     joinAC(x,meetAC(y,z)) -> meetAC(joinAC(x,y),joinAC(x,z))
    S:
     join{AC,#}(joinAC(x9,x10),x11) -> join{AC,#}(x9,x10)
     join{AC,#}(x9,joinAC(x10,x11)) -> join{AC,#}(x10,x11)
     meet{AC,#}(meetAC(x9,x10),x11) -> meet{AC,#}(x9,x10)
     meet{AC,#}(x9,meetAC(x10,x11)) -> meet{AC,#}(x10,x11)
    AC-DP unlabeling:
     Equations#:
      joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
      joinAC(x3,x4) -> joinAC(x4,x3)
      meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
      meetAC(x3,x4) -> meetAC(x4,x3)
      joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
      joinAC(x4,x3) -> joinAC(x3,x4)
      meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
      meetAC(x4,x3) -> meetAC(x3,x4)
     DPs:
      joinAC(x8,joinAC(x,meetAC(y,z))) -> joinAC(x8,meetAC(joinAC(x,y),joinAC(x,z)))
      joinAC(x8,joinAC(x,meetAC(y,z))) -> joinAC(x,y)
      joinAC(x8,joinAC(x,meetAC(y,z))) -> joinAC(x,z)
      joinAC(x6,joinAC(x,meetAC(x,y))) -> joinAC(x6,x)
      joinAC(x,meetAC(y,z)) -> joinAC(x,y)
      joinAC(x,meetAC(y,z)) -> joinAC(x,z)
     Equations:
      joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
      joinAC(x3,x4) -> joinAC(x4,x3)
      meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
      meetAC(x3,x4) -> meetAC(x4,x3)
      joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
      joinAC(x4,x3) -> joinAC(x3,x4)
      meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
      meetAC(x4,x3) -> meetAC(x3,x4)
     TRS:
      joinAC(x,meetAC(x,y)) -> x
      meetAC(x,joinAC(x,y)) -> x
      joinAC(x,meetAC(y,z)) -> meetAC(joinAC(x,y),joinAC(x,z))
     S:
      joinAC(joinAC(x9,x10),x11) -> joinAC(x9,x10)
      joinAC(x9,joinAC(x10,x11)) -> joinAC(x10,x11)
      meetAC(meetAC(x9,x10),x11) -> meetAC(x9,x10)
      meetAC(x9,meetAC(x10,x11)) -> meetAC(x10,x11)
     AC-RPO Processor:
      argument filtering:
       pi(joinAC) = [0,1]
       pi(meetAC) = [0,1]
      precedence:
       joinAC > meetAC
      status:
       
      problem:
       Equations#:
        joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
        joinAC(x3,x4) -> joinAC(x4,x3)
        meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
        meetAC(x3,x4) -> meetAC(x4,x3)
        joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
        joinAC(x4,x3) -> joinAC(x3,x4)
        meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
        meetAC(x4,x3) -> meetAC(x3,x4)
       DPs:
        
       Equations:
        joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
        joinAC(x3,x4) -> joinAC(x4,x3)
        meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
        meetAC(x3,x4) -> meetAC(x4,x3)
        joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
        joinAC(x4,x3) -> joinAC(x3,x4)
        meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
        meetAC(x4,x3) -> meetAC(x3,x4)
       TRS:
        joinAC(x,meetAC(x,y)) -> x
        meetAC(x,joinAC(x,y)) -> x
        joinAC(x,meetAC(y,z)) -> meetAC(joinAC(x,y),joinAC(x,z))
       S:
        joinAC(joinAC(x9,x10),x11) -> joinAC(x9,x10)
        joinAC(x9,joinAC(x10,x11)) -> joinAC(x10,x11)
        meetAC(meetAC(x9,x10),x11) -> meetAC(x9,x10)
        meetAC(x9,meetAC(x10,x11)) -> meetAC(x10,x11)
      Qed
    
    Equations#:
     join{AC,#}(joinAC(x3,x4),x5) -> join{AC,#}(x3,joinAC(x4,x5))
     join{AC,#}(x3,x4) -> join{AC,#}(x4,x3)
     meet{AC,#}(meetAC(x3,x4),x5) -> meet{AC,#}(x3,meetAC(x4,x5))
     meet{AC,#}(x3,x4) -> meet{AC,#}(x4,x3)
     join{AC,#}(x3,joinAC(x4,x5)) -> join{AC,#}(joinAC(x3,x4),x5)
     join{AC,#}(x4,x3) -> join{AC,#}(x3,x4)
     meet{AC,#}(x3,meetAC(x4,x5)) -> meet{AC,#}(meetAC(x3,x4),x5)
     meet{AC,#}(x4,x3) -> meet{AC,#}(x3,x4)
    DPs:
     meet{AC,#}(x7,meetAC(x,joinAC(x,y))) -> meet{AC,#}(x7,x)
    Equations:
     joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
     joinAC(x3,x4) -> joinAC(x4,x3)
     meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
     meetAC(x3,x4) -> meetAC(x4,x3)
     joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
     joinAC(x4,x3) -> joinAC(x3,x4)
     meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
     meetAC(x4,x3) -> meetAC(x3,x4)
    TRS:
     joinAC(x,meetAC(x,y)) -> x
     meetAC(x,joinAC(x,y)) -> x
     joinAC(x,meetAC(y,z)) -> meetAC(joinAC(x,y),joinAC(x,z))
    S:
     join{AC,#}(joinAC(x9,x10),x11) -> join{AC,#}(x9,x10)
     join{AC,#}(x9,joinAC(x10,x11)) -> join{AC,#}(x10,x11)
     meet{AC,#}(meetAC(x9,x10),x11) -> meet{AC,#}(x9,x10)
     meet{AC,#}(x9,meetAC(x10,x11)) -> meet{AC,#}(x10,x11)
    AC-DP unlabeling:
     Equations#:
      joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
      joinAC(x3,x4) -> joinAC(x4,x3)
      meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
      meetAC(x3,x4) -> meetAC(x4,x3)
      joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
      joinAC(x4,x3) -> joinAC(x3,x4)
      meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
      meetAC(x4,x3) -> meetAC(x3,x4)
     DPs:
      meetAC(x7,meetAC(x,joinAC(x,y))) -> meetAC(x7,x)
     Equations:
      joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
      joinAC(x3,x4) -> joinAC(x4,x3)
      meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
      meetAC(x3,x4) -> meetAC(x4,x3)
      joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
      joinAC(x4,x3) -> joinAC(x3,x4)
      meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
      meetAC(x4,x3) -> meetAC(x3,x4)
     TRS:
      joinAC(x,meetAC(x,y)) -> x
      meetAC(x,joinAC(x,y)) -> x
      joinAC(x,meetAC(y,z)) -> meetAC(joinAC(x,y),joinAC(x,z))
     S:
      joinAC(joinAC(x9,x10),x11) -> joinAC(x9,x10)
      joinAC(x9,joinAC(x10,x11)) -> joinAC(x10,x11)
      meetAC(meetAC(x9,x10),x11) -> meetAC(x9,x10)
      meetAC(x9,meetAC(x10,x11)) -> meetAC(x10,x11)
     Usable Rule Processor:
      Equations#:
       joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
       joinAC(x3,x4) -> joinAC(x4,x3)
       meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
       meetAC(x3,x4) -> meetAC(x4,x3)
       joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
       joinAC(x4,x3) -> joinAC(x3,x4)
       meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
       meetAC(x4,x3) -> meetAC(x3,x4)
      DPs:
       meetAC(x7,meetAC(x,joinAC(x,y))) -> meetAC(x7,x)
      Equations:
       joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
       joinAC(x3,x4) -> joinAC(x4,x3)
       meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
       meetAC(x3,x4) -> meetAC(x4,x3)
       joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
       joinAC(x4,x3) -> joinAC(x3,x4)
       meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
       meetAC(x4,x3) -> meetAC(x3,x4)
      TRS:
       meetAC(x,joinAC(x,y)) -> x
      S:
       joinAC(joinAC(x9,x10),x11) -> joinAC(x9,x10)
       joinAC(x9,joinAC(x10,x11)) -> joinAC(x10,x11)
       meetAC(meetAC(x9,x10),x11) -> meetAC(x9,x10)
       meetAC(x9,meetAC(x10,x11)) -> meetAC(x10,x11)
      AC-RPO Processor:
       argument filtering:
        pi(joinAC) = []
        pi(meetAC) = [0,1]
       precedence:
        meetAC > joinAC
       status:
        
       problem:
        Equations#:
         joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
         joinAC(x3,x4) -> joinAC(x4,x3)
         meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
         meetAC(x3,x4) -> meetAC(x4,x3)
         joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
         joinAC(x4,x3) -> joinAC(x3,x4)
         meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
         meetAC(x4,x3) -> meetAC(x3,x4)
        DPs:
         
        Equations:
         joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
         joinAC(x3,x4) -> joinAC(x4,x3)
         meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
         meetAC(x3,x4) -> meetAC(x4,x3)
         joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
         joinAC(x4,x3) -> joinAC(x3,x4)
         meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
         meetAC(x4,x3) -> meetAC(x3,x4)
        TRS:
         meetAC(x,joinAC(x,y)) -> x
        S:
         joinAC(joinAC(x9,x10),x11) -> joinAC(x9,x10)
         joinAC(x9,joinAC(x10,x11)) -> joinAC(x10,x11)
         meetAC(meetAC(x9,x10),x11) -> meetAC(x9,x10)
         meetAC(x9,meetAC(x10,x11)) -> meetAC(x10,x11)
       Qed