Ei(EF(Cyclin)).
Ei(EF(!(Cyclin))).
Ai(AG(Cyclin->EF(!(Cyclin))&(!(Cyclin)->EF(Cyclin)))).
Ei(EF(Cdc2~{p1})).
Ei(EF(!(Cdc2~{p1}))).
Ai(AG(Cdc2~{p1}->EF(!(Cdc2~{p1}))&(!(Cdc2~{p1})->EF(Cdc2~{p1})))).
Ai(AG(!(Cdc2~{p1})->!(E(!(Cdc2) U Cdc2~{p1})))).
Ei(EF(Cdc2-Cyclin~{p1,p2})).
Ei(EF(!(Cdc2-Cyclin~{p1,p2}))).
Ai(AG(Cdc2-Cyclin~{p1,p2}->EF(!(Cdc2-Cyclin~{p1,p2}))&(!(Cdc2-Cyclin~{p1,p2})->EF(Cdc2-Cyclin~{p1,p2})))).
Ei(EF(Cdc2-Cyclin~{p1})).
Ei(EF(!(Cdc2-Cyclin~{p1}))).
Ai(AG(Cdc2-Cyclin~{p1}->EF(!(Cdc2-Cyclin~{p1}))&(!(Cdc2-Cyclin~{p1})->EF(Cdc2-Cyclin~{p1})))).
Ai(AG(!(Cdc2-Cyclin~{p1})->!(E(!(Cdc2-Cyclin~{p1,p2}) U Cdc2-Cyclin~{p1})))).
Ei(EF(Cdc2)).
Ei(EF(!(Cdc2))).
Ai(AG(Cdc2->EF(!(Cdc2))&(!(Cdc2)->EF(Cdc2)))).
Ei(EF(Cyclin~{p1})).
Ei(EF(!(Cyclin~{p1}))).
Ai(AG(Cyclin~{p1}->EF(!(Cyclin~{p1}))&(!(Cyclin~{p1})->EF(Cyclin~{p1})))).
Ai(AG(!(Cyclin~{p1})->!(E(!(Cdc2-Cyclin~{p1}) U Cyclin~{p1})))).