YES
Time: 0.154

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:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                                [0]
   [meetAC](x0, x1) = x0 + x1 + [9],
   
                                [4]
   [joinAC](x0, x1) = x0 + x1 + [4]
  orientation:
                           [2 0]        [4 ]         
   joinAC(x,meetAC(x,y)) = [0 2]x + y + [13] >= x = x
   
                           [2 0]        [4 ]         
   meetAC(x,joinAC(x,y)) = [0 2]x + y + [13] >= x = 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)
   TRS:
    
  Qed