<eventually1 , PreSafety, gamma=0.8> Pmax=? [ F<1  "picked_up_blue_key" ];
<eventually2 , PreSafety, gamma=0.8> Pmax=? [ F<2  "picked_up_blue_key" ];
<eventually3 , PreSafety, gamma=0.8> Pmax=? [ F<3  "picked_up_blue_key" ];
<eventually4 , PreSafety, gamma=0.8> Pmax=? [ F<4  "picked_up_blue_key" ];
<eventually5 , PreSafety, gamma=0.8> Pmax=? [ F<5  "picked_up_blue_key" ];
<eventually6 , PreSafety, gamma=0.8> Pmax=? [ F<6  "picked_up_blue_key" ];
<eventually7 , PreSafety, gamma=0.8> Pmax=? [ F<7  "picked_up_blue_key" ];
<eventually8 , PreSafety, gamma=0.8> Pmax=? [ F<8  "picked_up_blue_key" ];
<eventually9 , PreSafety, gamma=0.8> Pmax=? [ F<9  "picked_up_blue_key" ];
<eventually10, PreSafety, gamma=0.8> Pmax=? [ F<10 "picked_up_blue_key" ];
<eventually11, PreSafety, gamma=0.8> Pmax=? [ F<11 "picked_up_blue_key" ];
<eventually12, PreSafety, gamma=0.8> Pmax=? [ F<12 "picked_up_blue_key" ];
<eventually13, PreSafety, gamma=0.8> Pmax=? [ F<13 "picked_up_blue_key" ];
<eventually14, PreSafety, gamma=0.8> Pmax=? [ F<14 "picked_up_blue_key" ];
<eventually15, PreSafety, gamma=0.8> Pmax=? [ F<15 "picked_up_blue_key" ];
<eventually16, PreSafety, gamma=0.8> Pmax=? [ F<16 "picked_up_blue_key" ];
<eventually17, PreSafety, gamma=0.8> Pmax=? [ F<17 "picked_up_blue_key" ];
<eventually18, PreSafety, gamma=0.8> Pmax=? [ F<18 "picked_up_blue_key" ];
<eventually19, PreSafety, gamma=0.8> Pmax=? [ F<19 "picked_up_blue_key" ];
<eventually20, PreSafety, gamma=0.8> Pmax=? [ F<20 "picked_up_blue_key" ];