YES
Time: 0.010

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:
 AC-KBO Processor:
  precedence:
   meetAC ~ joinAC
   weight function:
    w0 = 4
    w(meetAC) = w(joinAC) = 0
   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:
     
   Qed