// Nonzero-sum properties (N-player)

// expected time each user eventually sends a packet
<<usr1:usr2:usr3:usr4:usr5>>{NE,SW}min=? (R{"time"}[F s1=3] + R{"time"}[F s2=3] + R{"time"}[F s3=3] + R{"time"}[F s4=3] + R{"time"}[F s5=3])
<<usr1:usr2:usr3:usr4:usr5>>{NE,FR}min=? (R{"time"}[F s1=3] + R{"time"}[F s2=3] + R{"time"}[F s3=3] + R{"time"}[F s4=3] + R{"time"}[F s5=3])
<<usr1:usr2:usr3:usr4:usr5>>{CE,SW}min=? (R{"time"}[F s1=3] + R{"time"}[F s2=3] + R{"time"}[F s3=3] + R{"time"}[F s4=3] + R{"time"}[F s5=3])
<<usr1:usr2:usr3:usr4:usr5>>{CE,FR}min=? (R{"time"}[F s1=3] + R{"time"}[F s2=3] + R{"time"}[F s3=3] + R{"time"}[F s4=3] + R{"time"}[F s5=3])

// probability each user eventually sents a packet within a deadline
<<usr1:usr2:usr3:usr4:usr5>>{NE,SW}max=? (P[F (s1=3 & t<=D)] + P[F (s2=3 & t<=D)] + P[F (s3=3 & t<=D)] + P[F (s4=3 & t<=D)] + P[F (s5=3 & t<=D)])
<<usr1:usr2:usr3:usr4:usr5>>{NE,FR}max=? (P[F (s1=3 & t<=D)] + P[F (s2=3 & t<=D)] + P[F (s3=3 & t<=D)] + P[F (s4=3 & t<=D)] + P[F (s5=3 & t<=D)])
<<usr1:usr2:usr3:usr4:usr5>>{CE,SW}max=? (P[F (s1=3 & t<=D)] + P[F (s2=3 & t<=D)] + P[F (s3=3 & t<=D)] + P[F (s4=3 & t<=D)] + P[F (s5=3 & t<=D)])
<<usr1:usr2:usr3:usr4:usr5>>{CE,FR}max=? (P[F (s1=3 & t<=D)] + P[F (s2=3 & t<=D)] + P[F (s3=3 & t<=D)] + P[F (s4=3 & t<=D)] + P[F (s5=3 & t<=D)])