YES
Time: 0.008

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:
    [meetAC](x0, x1) = x0 + x1,
    
    [joinAC](x0, x1) = x0 + x1
   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