val f1a = Ef (And(Pred "Pspeak", Pred "TgetFloor"));
val f1b = And(Ag(Imply(Pred "Pspeak", Not(Pred "TgetFloor"))), Ag (Imply(Pred "TgetFloor", Not(Pred "Pspeak"))));
val f2 = Ag(Imply(Not(Pred "Pmoderate"),Pred "Phold"));
val f3 = Ag(Imply(Pred "Phold",Ax(Af(Not(Pred "Phold")))));
val f4 = Ag(Imply(Pred "Pwait", Ax(Af(Not(Pred "Pwait")))));
val f5 = Or(Ag(Pred "Pmoderate"),Au(Not(Pred "Pmoderate"),Pred "Pmoderate"));
val f6 = Ef(And(Not(Pred "Pmoderate"),Pred "TgrabFloor"));