Ei(EF(RAF)).
Ei(EF(!(RAF))).
Ai(AG(RAF->EF(!(RAF))&(!(RAF)->EF(RAF)))).
Ei(EF(RAFK)).
Ei(EF(!(RAFK))).
Ai(AG(RAFK->EF(!(RAFK))&(!(RAFK)->EF(RAFK)))).
Ai(AG(!(RAFK)->!(E(!(RAF-RAFK) U RAFK)))).
Ei(EF(RAF-RAFK)).
Ei(EF(!(RAF-RAFK))).
Ai(AG(RAF-RAFK->EF(!(RAF-RAFK))&(!(RAF-RAFK)->EF(RAF-RAFK)))).
Ai(AG(!(RAF-RAFK)->!(E(!(RAF) U RAF-RAFK)))).
Ai(AG(!(RAF-RAFK)->!(E(!(RAFK) U RAF-RAFK)))).
Ei(EF(RAFPH)).
Ei(EF(!(RAFPH))).
Ai(AG(RAFPH->EF(!(RAFPH))&(!(RAFPH)->EF(RAFPH)))).
Ai(AG(!(RAFPH)->!(E(!(RAFPH-RAF~{p1}) U RAFPH)))).
Ei(EF(RAF~{p1})).
Ei(EF(!(RAF~{p1}))).
Ai(AG(RAF~{p1}->EF(!(RAF~{p1}))&(!(RAF~{p1})->EF(RAF~{p1})))).
Ei(EF(RAFPH-RAF~{p1})).
Ei(EF(!(RAFPH-RAF~{p1}))).
Ai(AG(RAFPH-RAF~{p1}->EF(!(RAFPH-RAF~{p1}))&(!(RAFPH-RAF~{p1})->EF(RAFPH-RAF~{p1})))).
Ai(AG(!(RAFPH-RAF~{p1})->!(E(!(RAFPH) U RAFPH-RAF~{p1})))).
Ai(AG(!(RAFPH-RAF~{p1})->!(E(!(RAF~{p1}) U RAFPH-RAF~{p1})))).
Ei(EF(MEK)).
Ei(EF(!(MEK))).
Ai(AG(MEK->EF(!(MEK))&(!(MEK)->EF(MEK)))).
Ei(EF(MEK-RAF~{p1})).
Ei(EF(!(MEK-RAF~{p1}))).
Ai(AG(MEK-RAF~{p1}->EF(!(MEK-RAF~{p1}))&(!(MEK-RAF~{p1})->EF(MEK-RAF~{p1})))).
Ai(AG(!(MEK-RAF~{p1})->!(E(!(MEK) U MEK-RAF~{p1})))).
Ai(AG(!(MEK-RAF~{p1})->!(E(!(RAF~{p1}) U MEK-RAF~{p1})))).
Ei(EF(MEK~{p1})).
Ei(EF(!(MEK~{p1}))).
Ai(AG(MEK~{p1}->EF(!(MEK~{p1}))&(!(MEK~{p1})->EF(MEK~{p1})))).
Ei(EF(MEK~{p1}-RAF~{p1})).
Ei(EF(!(MEK~{p1}-RAF~{p1}))).
Ai(AG(MEK~{p1}-RAF~{p1}->EF(!(MEK~{p1}-RAF~{p1}))&(!(MEK~{p1}-RAF~{p1})->EF(MEK~{p1}-RAF~{p1})))).
Ai(AG(!(MEK~{p1}-RAF~{p1})->!(E(!(RAF~{p1}) U MEK~{p1}-RAF~{p1})))).
Ai(AG(!(MEK~{p1}-RAF~{p1})->!(E(!(MEK~{p1}) U MEK~{p1}-RAF~{p1})))).
Ei(EF(MEKPH)).
Ei(EF(!(MEKPH))).
Ai(AG(MEKPH->EF(!(MEKPH))&(!(MEKPH)->EF(MEKPH)))).
Ei(EF(MEKPH-MEK~{p1})).
Ei(EF(!(MEKPH-MEK~{p1}))).
Ai(AG(MEKPH-MEK~{p1}->EF(!(MEKPH-MEK~{p1}))&(!(MEKPH-MEK~{p1})->EF(MEKPH-MEK~{p1})))).
Ai(AG(!(MEKPH-MEK~{p1})->!(E(!(MEKPH) U MEKPH-MEK~{p1})))).
Ai(AG(!(MEKPH-MEK~{p1})->!(E(!(MEK~{p1}) U MEKPH-MEK~{p1})))).
Ei(EF(MEK~{p1,p2})).
Ei(EF(!(MEK~{p1,p2}))).
Ai(AG(MEK~{p1,p2}->EF(!(MEK~{p1,p2}))&(!(MEK~{p1,p2})->EF(MEK~{p1,p2})))).
Ei(EF(MEKPH-MEK~{p1,p2})).
Ei(EF(!(MEKPH-MEK~{p1,p2}))).
Ai(AG(MEKPH-MEK~{p1,p2}->EF(!(MEKPH-MEK~{p1,p2}))&(!(MEKPH-MEK~{p1,p2})->EF(MEKPH-MEK~{p1,p2})))).
Ai(AG(!(MEKPH-MEK~{p1,p2})->!(E(!(MEKPH) U MEKPH-MEK~{p1,p2})))).
Ai(AG(!(MEKPH-MEK~{p1,p2})->!(E(!(MEK~{p1,p2}) U MEKPH-MEK~{p1,p2})))).
Ei(EF(MAPK)).
Ei(EF(!(MAPK))).
Ai(AG(MAPK->EF(!(MAPK))&(!(MAPK)->EF(MAPK)))).
Ei(EF(MAPK-MEK~{p1,p2})).
Ei(EF(!(MAPK-MEK~{p1,p2}))).
Ai(AG(MAPK-MEK~{p1,p2}->EF(!(MAPK-MEK~{p1,p2}))&(!(MAPK-MEK~{p1,p2})->EF(MAPK-MEK~{p1,p2})))).
Ai(AG(!(MAPK-MEK~{p1,p2})->!(E(!(MAPK) U MAPK-MEK~{p1,p2})))).
Ai(AG(!(MAPK-MEK~{p1,p2})->!(E(!(MEK~{p1,p2}) U MAPK-MEK~{p1,p2})))).
Ei(EF(MAPK~{p1})).
Ei(EF(!(MAPK~{p1}))).
Ai(AG(MAPK~{p1}->EF(!(MAPK~{p1}))&(!(MAPK~{p1})->EF(MAPK~{p1})))).
Ei(EF(MAPK~{p1}-MEK~{p1,p2})).
Ei(EF(!(MAPK~{p1}-MEK~{p1,p2}))).
Ai(AG(MAPK~{p1}-MEK~{p1,p2}->EF(!(MAPK~{p1}-MEK~{p1,p2}))&(!(MAPK~{p1}-MEK~{p1,p2})->EF(MAPK~{p1}-MEK~{p1,p2})))).
Ai(AG(!(MAPK~{p1}-MEK~{p1,p2})->!(E(!(MEK~{p1,p2}) U MAPK~{p1}-MEK~{p1,p2})))).
Ai(AG(!(MAPK~{p1}-MEK~{p1,p2})->!(E(!(MAPK~{p1}) U MAPK~{p1}-MEK~{p1,p2})))).
Ei(EF(MAPKPH)).
Ei(EF(!(MAPKPH))).
Ai(AG(MAPKPH->EF(!(MAPKPH))&(!(MAPKPH)->EF(MAPKPH)))).
Ei(EF(MAPKPH-MAPK~{p1})).
Ei(EF(!(MAPKPH-MAPK~{p1}))).
Ai(AG(MAPKPH-MAPK~{p1}->EF(!(MAPKPH-MAPK~{p1}))&(!(MAPKPH-MAPK~{p1})->EF(MAPKPH-MAPK~{p1})))).
Ai(AG(!(MAPKPH-MAPK~{p1})->!(E(!(MAPKPH) U MAPKPH-MAPK~{p1})))).
Ai(AG(!(MAPKPH-MAPK~{p1})->!(E(!(MAPK~{p1}) U MAPKPH-MAPK~{p1})))).
Ei(EF(MAPK~{p1,p2})).
Ei(EF(!(MAPK~{p1,p2}))).
Ai(AG(MAPK~{p1,p2}->EF(!(MAPK~{p1,p2}))&(!(MAPK~{p1,p2})->EF(MAPK~{p1,p2})))).
Ei(EF(MAPKPH-MAPK~{p1,p2})).
Ei(EF(!(MAPKPH-MAPK~{p1,p2}))).
Ai(AG(MAPKPH-MAPK~{p1,p2}->EF(!(MAPKPH-MAPK~{p1,p2}))&(!(MAPKPH-MAPK~{p1,p2})->EF(MAPKPH-MAPK~{p1,p2})))).Ai(AG(!(MAPKPH-MAPK~{p1,p2})->!(E(!(MAPKPH) U MAPKPH-MAPK~{p1,p2})))).
Ai(AG(!(MAPKPH-MAPK~{p1,p2})->!(E(!(MAPK~{p1,p2}) U MAPKPH-MAPK~{p1,p2})))).