YES
Time: 0.025

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: 1
  interpretation:
   [meetAC](x0, x1) = x0 + x1 + 2,
   
   [joinAC](x0, x1) = x0 + x1
  orientation:
   joinAC(x,meetAC(x,y)) = 2x + y + 2 >= x = x
   
   meetAC(x,joinAC(x,y)) = 2x + y + 2 >= 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