Undecidability of Model Checking in Brane Logic