// maximum probability the user can ensure that at least half their messages are sent
<<user>> Pmax=? [ F sent>=slots/2 ]

const int k;
// maximum expected number of messages the user can ensure are sent after k slots
<<user>> R{"rew"}max=? [ I=k ]