YES
Time: 0.016

Problem:
 Equations:
  meetAC(meetAC(x1,x2),x3) -> meetAC(x1,meetAC(x2,x3))
  meetAC(x1,x2) -> meetAC(x2,x1)
  meetAC(x1,meetAC(x2,x3)) -> meetAC(meetAC(x1,x2),x3)
  meetAC(x2,x1) -> meetAC(x1,x2)
 TRS:
  meetAC(x,x) -> x

Proof:
 DP Processor:
  Equations#:
   meet{AC,#}(meetAC(x1,x2),x3) -> meet{AC,#}(x1,meetAC(x2,x3))
   meet{AC,#}(x1,x2) -> meet{AC,#}(x2,x1)
   meet{AC,#}(x1,meetAC(x2,x3)) -> meet{AC,#}(meetAC(x1,x2),x3)
   meet{AC,#}(x2,x1) -> meet{AC,#}(x1,x2)
  DPs:
   meet{AC,#}(x4,meetAC(x,x)) -> meet{AC,#}(x4,x)
  Equations:
   meetAC(meetAC(x1,x2),x3) -> meetAC(x1,meetAC(x2,x3))
   meetAC(x1,x2) -> meetAC(x2,x1)
   meetAC(x1,meetAC(x2,x3)) -> meetAC(meetAC(x1,x2),x3)
   meetAC(x2,x1) -> meetAC(x1,x2)
  TRS:
   meetAC(x,x) -> x
  S:
   meet{AC,#}(meetAC(x5,x6),x7) -> meet{AC,#}(x5,x6)
   meet{AC,#}(x5,meetAC(x6,x7)) -> meet{AC,#}(x6,x7)
  AC-DP unlabeling:
   Equations#:
    meetAC(meetAC(x1,x2),x3) -> meetAC(x1,meetAC(x2,x3))
    meetAC(x1,x2) -> meetAC(x2,x1)
    meetAC(x1,meetAC(x2,x3)) -> meetAC(meetAC(x1,x2),x3)
    meetAC(x2,x1) -> meetAC(x1,x2)
   DPs:
    meetAC(x4,meetAC(x,x)) -> meetAC(x4,x)
   Equations:
    meetAC(meetAC(x1,x2),x3) -> meetAC(x1,meetAC(x2,x3))
    meetAC(x1,x2) -> meetAC(x2,x1)
    meetAC(x1,meetAC(x2,x3)) -> meetAC(meetAC(x1,x2),x3)
    meetAC(x2,x1) -> meetAC(x1,x2)
   TRS:
    meetAC(x,x) -> x
   S:
    meetAC(meetAC(x5,x6),x7) -> meetAC(x5,x6)
    meetAC(x5,meetAC(x6,x7)) -> meetAC(x6,x7)
   AC-KBO Processor:
    argument filtering:
     pi(meetAC) = [0,1]
    precedence:
     meetAC
     weight function:
      [meetAC](x0, x1) = x0 + x1
      usable rules:
       meetAC(x,x) -> x
      problem:
       Equations#:
        meetAC(meetAC(x1,x2),x3) -> meetAC(x1,meetAC(x2,x3))
        meetAC(x1,x2) -> meetAC(x2,x1)
        meetAC(x1,meetAC(x2,x3)) -> meetAC(meetAC(x1,x2),x3)
        meetAC(x2,x1) -> meetAC(x1,x2)
       DPs:
        
       Equations:
        meetAC(meetAC(x1,x2),x3) -> meetAC(x1,meetAC(x2,x3))
        meetAC(x1,x2) -> meetAC(x2,x1)
        meetAC(x1,meetAC(x2,x3)) -> meetAC(meetAC(x1,x2),x3)
        meetAC(x2,x1) -> meetAC(x1,x2)
       TRS:
        meetAC(x,x) -> x
       S:
        meetAC(meetAC(x5,x6),x7) -> meetAC(x5,x6)
        meetAC(x5,meetAC(x6,x7)) -> meetAC(x6,x7)
      Qed