Ei(EF(CycB)).
Ei(EF(!(CycB))).
Ai(AG(CycB->EF(!(CycB))&(!(CycB)->EF(CycB)))).
Ei(EF(APC)).
Ei(EF(!(APC))).
Ai(AG(APC->EF(!(APC))&(!(APC)->EF(APC)))).
Ai(AG(!(APC)->!(E(!(CycB-CDK~{p1}) U APC)))).
Ei(EF(CDK)).
Ei(EF(!(CDK))).
Ai(AG(CDK->EF(!(CDK))&(!(CDK)->EF(CDK)))).
Ei(EF(CycB-CDK~{p1,p2})).
Ei(EF(!(CycB-CDK~{p1,p2}))).
Ai(AG(CycB-CDK~{p1,p2}->EF(!(CycB-CDK~{p1,p2}))&(!(CycB-CDK~{p1,p2})->EF(CycB-CDK~{p1,p2})))).
Ei(EF(CycB-CDK~{p1})).
Ei(EF(!(CycB-CDK~{p1}))).
Ai(AG(CycB-CDK~{p1}->EF(!(CycB-CDK~{p1}))&(!(CycB-CDK~{p1})->EF(CycB-CDK~{p1})))).
Ei(EF(C25~{p1,p2})).
Ei(EF(!(C25~{p1,p2}))).
Ai(AG(C25~{p1,p2}->EF(!(C25~{p1,p2}))&(!(C25~{p1,p2})->EF(C25~{p1,p2})))).
Ai(AG(!(C25~{p1,p2})->!(E(!(C25~{p1}) U C25~{p1,p2})))).
Ei(EF(Wee1)).
Ei(EF(!(Wee1))).
Ai(AG(Wee1->EF(!(Wee1))&(!(Wee1)->EF(Wee1)))).
Ei(EF(C25)).
Ei(EF(!(C25))).
Ai(AG(C25->EF(!(C25))&(!(C25)->EF(C25)))).
Ei(EF(C25~{p1})).
Ei(EF(!(C25~{p1}))).
Ai(AG(C25~{p1}->EF(!(C25~{p1}))&(!(C25~{p1})->EF(C25~{p1})))).
Ei(EF(Wee1~{p1})).
Ei(EF(!(Wee1~{p1}))).
Ai(AG(Wee1~{p1}->EF(!(Wee1~{p1}))&(!(Wee1~{p1})->EF(Wee1~{p1})))).
Ai(AG(!(Wee1~{p1})->!(E(!(Wee1) U Wee1~{p1})))).
Ei(EF(CKI)).
Ei(EF(!(CKI))).
Ai(AG(CKI->EF(!(CKI))&(!(CKI)->EF(CKI)))).
Ei(EF(CKI-CycB-CDK~{p1})).
Ei(EF(!(CKI-CycB-CDK~{p1}))).
Ai(AG(CKI-CycB-CDK~{p1}->EF(!(CKI-CycB-CDK~{p1}))&(!(CKI-CycB-CDK~{p1})->EF(CKI-CycB-CDK~{p1})))).
Ei(EF((CKI-CycB-CDK~{p1})~{p2})).
Ei(EF(!((CKI-CycB-CDK~{p1})~{p2}))).
Ai(AG((CKI-CycB-CDK~{p1})~{p2}->EF(!((CKI-CycB-CDK~{p1})~{p2}))&(!((CKI-CycB-CDK~{p1})~{p2})->EF((CKI-CycB-CDK~{p1})~{p2})))).
Ai(AG(!((CKI-CycB-CDK~{p1})~{p2})->!(E(!(CKI-CycB-CDK~{p1}) U (CKI-CycB-CDK~{p1})~{p2})))).