MAYBE
Time: 0.165

Problem:
 Equations:
  joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
  joinAC(x3,x4) -> joinAC(x4,x3)
  meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
  meetAC(x3,x4) -> meetAC(x4,x3)
  joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
  joinAC(x4,x3) -> joinAC(x3,x4)
  meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
  meetAC(x4,x3) -> meetAC(x3,x4)
 TRS:
  joinAC(x,meetAC(x,y)) -> x
  meetAC(x,joinAC(x,y)) -> x
  joinAC(x,meetAC(y,z)) -> meetAC(joinAC(x,y),joinAC(x,z))

Proof:
 DP Processor:
  Equations#:
   join{AC,#}(joinAC(x3,x4),x5) -> join{AC,#}(x3,joinAC(x4,x5))
   join{AC,#}(x3,x4) -> join{AC,#}(x4,x3)
   meet{AC,#}(meetAC(x3,x4),x5) -> meet{AC,#}(x3,meetAC(x4,x5))
   meet{AC,#}(x3,x4) -> meet{AC,#}(x4,x3)
   join{AC,#}(x3,joinAC(x4,x5)) -> join{AC,#}(joinAC(x3,x4),x5)
   join{AC,#}(x4,x3) -> join{AC,#}(x3,x4)
   meet{AC,#}(x3,meetAC(x4,x5)) -> meet{AC,#}(meetAC(x3,x4),x5)
   meet{AC,#}(x4,x3) -> meet{AC,#}(x3,x4)
  DPs:
   join{AC,#}(x,meetAC(y,z)) -> join{AC,#}(x,z)
   join{AC,#}(x,meetAC(y,z)) -> join{AC,#}(x,y)
   join{AC,#}(x,meetAC(y,z)) -> meet{AC,#}(joinAC(x,y),joinAC(x,z))
   join{AC,#}(x6,joinAC(x,meetAC(x,y))) -> join{AC,#}(x6,x)
   meet{AC,#}(x7,meetAC(x,joinAC(x,y))) -> meet{AC,#}(x7,x)
   join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x,z)
   join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x,y)
   join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> meet{AC,#}(joinAC(x,y),joinAC(x,z))
   join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x8,meetAC(joinAC(x,y),joinAC(x,z)))
  Equations:
   joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
   joinAC(x3,x4) -> joinAC(x4,x3)
   meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
   meetAC(x3,x4) -> meetAC(x4,x3)
   joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
   joinAC(x4,x3) -> joinAC(x3,x4)
   meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
   meetAC(x4,x3) -> meetAC(x3,x4)
  TRS:
   joinAC(x,meetAC(x,y)) -> x
   meetAC(x,joinAC(x,y)) -> x
   joinAC(x,meetAC(y,z)) -> meetAC(joinAC(x,y),joinAC(x,z))
  S:
   join{AC,#}(joinAC(x9,x10),x11) -> join{AC,#}(x9,x10)
   join{AC,#}(x9,joinAC(x10,x11)) -> join{AC,#}(x10,x11)
   meet{AC,#}(meetAC(x9,x10),x11) -> meet{AC,#}(x9,x10)
   meet{AC,#}(x9,meetAC(x10,x11)) -> meet{AC,#}(x10,x11)
  AC-EDG Processor:
   Equations#:
    join{AC,#}(joinAC(x3,x4),x5) -> join{AC,#}(x3,joinAC(x4,x5))
    join{AC,#}(x3,x4) -> join{AC,#}(x4,x3)
    meet{AC,#}(meetAC(x3,x4),x5) -> meet{AC,#}(x3,meetAC(x4,x5))
    meet{AC,#}(x3,x4) -> meet{AC,#}(x4,x3)
    join{AC,#}(x3,joinAC(x4,x5)) -> join{AC,#}(joinAC(x3,x4),x5)
    join{AC,#}(x4,x3) -> join{AC,#}(x3,x4)
    meet{AC,#}(x3,meetAC(x4,x5)) -> meet{AC,#}(meetAC(x3,x4),x5)
    meet{AC,#}(x4,x3) -> meet{AC,#}(x3,x4)
   DPs:
    join{AC,#}(x,meetAC(y,z)) -> join{AC,#}(x,z)
    join{AC,#}(x,meetAC(y,z)) -> join{AC,#}(x,y)
    join{AC,#}(x,meetAC(y,z)) -> meet{AC,#}(joinAC(x,y),joinAC(x,z))
    join{AC,#}(x6,joinAC(x,meetAC(x,y))) -> join{AC,#}(x6,x)
    meet{AC,#}(x7,meetAC(x,joinAC(x,y))) -> meet{AC,#}(x7,x)
    join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x,z)
    join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x,y)
    join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> meet{AC,#}(joinAC(x,y),joinAC(x,z))
    join{AC,#}(x8,joinAC(x,meetAC(y,z))) -> join{AC,#}(x8,meetAC(joinAC(x,y),joinAC(x,z)))
   Equations:
    joinAC(joinAC(x3,x4),x5) -> joinAC(x3,joinAC(x4,x5))
    joinAC(x3,x4) -> joinAC(x4,x3)
    meetAC(meetAC(x3,x4),x5) -> meetAC(x3,meetAC(x4,x5))
    meetAC(x3,x4) -> meetAC(x4,x3)
    joinAC(x3,joinAC(x4,x5)) -> joinAC(joinAC(x3,x4),x5)
    joinAC(x4,x3) -> joinAC(x3,x4)
    meetAC(x3,meetAC(x4,x5)) -> meetAC(meetAC(x3,x4),x5)
    meetAC(x4,x3) -> meetAC(x3,x4)
   TRS:
    joinAC(x,meetAC(x,y)) -> x
    meetAC(x,joinAC(x,y)) -> x
    joinAC(x,meetAC(y,z)) -> meetAC(joinAC(x,y),joinAC(x,z))
   S:
    join{AC,#}(joinAC(x9,x10),x11) -> join{AC,#}(x9,x10)
    join{AC,#}(x9,joinAC(x10,x11)) -> join{AC,#}(x10,x11)
    meet{AC,#}(meetAC(x9,x10),x11) -> meet{AC,#}(x9,x10)
    meet{AC,#}(x9,meetAC(x10,x11)) -> meet{AC,#}(x10,x11)
   Open