MAYBE
Time: 0.812

Problem:
 Equations:
  eqAC(eqAC(x3,x4),x5) -> eqAC(x3,eqAC(x4,x5))
  eqAC(x3,x4) -> eqAC(x4,x3)
  unionAC(unionAC(x3,x4),x5) -> unionAC(x3,unionAC(x4,x5))
  unionAC(x3,x4) -> unionAC(x4,x3)
  interAC(interAC(x3,x4),x5) -> interAC(x3,interAC(x4,x5))
  interAC(x3,x4) -> interAC(x4,x3)
  eqAC(x3,eqAC(x4,x5)) -> eqAC(eqAC(x3,x4),x5)
  eqAC(x4,x3) -> eqAC(x3,x4)
  unionAC(x3,unionAC(x4,x5)) -> unionAC(unionAC(x3,x4),x5)
  unionAC(x4,x3) -> unionAC(x3,x4)
  interAC(x3,interAC(x4,x5)) -> interAC(interAC(x3,x4),x5)
  interAC(x4,x3) -> interAC(x3,x4)
 TRS:
  if(true(),x,y) -> x
  if(false(),x,y) -> y
  eqAC(0(),0()) -> true()
  eqAC(0(),1()) -> false()
  eqAC(1(),1()) -> true()
  unionAC(empty(),x) -> x
  interAC(x,empty()) -> empty()
  interAC(x,unionAC(y,z)) -> unionAC(interAC(x,y),interAC(x,z))
  interAC(single(x),single(y)) -> if(eqAC(x,y),single(x),empty())

Proof:
 Open