// Maximum expected reward achievable in the game
// Result: 11.999999999999998
<<ag1, ag3, sched, ag2>> R{"Coalition123"}max=? [ Fc target ]

// Minimum expected reward achievable in the game
// Result: 1.3333333333333333
<<ag1, ag3, sched, ag2>> R{"Coalition123"}min=? [ Fc target ]

// Maximum reward that can be achieved by coalition of two agents and the scheduler
// Result: 5.333333333333333
<<ag1, sched, ag2>> R{"Coalition12"}max=? [ Fc target ]

// Minimum reward that can be achieved by coalition of two agents and the scheduler
// Result: 3.666666666666666
<<ag1, sched, ag2>> R{"Coalition12"}min=? [ Fc target ]

// Maximum reward that can be achieved by coalition of two agents
// Result: 5.333333333333333
<<ag1, ag2>> R{"Coalition12"}max=? [ Fc target ]

// Minimum reward that can be achieved by coalition of two agents
// Result: 3.666666666666666 
<<ag1, ag2>> R{"Coalition12"}min=? [ Fc target ]

// Maximum reward that can be achieved by one agent
// Result: 1.3333333333333333 
<<ag1>> R{"Coalition1"}max=? [ Fc target ]

// Minimum reward that can be achieved by one agent
// Result: 2.6666666666666665
<<ag1>> R{"Coalition1"}min=? [ Fc target ]

// Maximum probability that two agents and a scheduler can guarantee to achieve a cooperating pair
// Result: 0.3333333333333333
<<ag1, sched, ag2>> Pmax=? [ F cooperating ]

// Maximum probability that two agents can guarantee to achieve a cooperating or defecting pair
// Result: 0.3333333333333333
<<ag1, ag2>> Pmax=? [ F cooperating|defecting ]

// Maximum probability that two agents and a scheduler can guarantee to achieve a cooperating or defecting pair
// Result: 1.0
<<ag1, sched, ag2>> Pmax=? [ F cooperating|defecting ]

<<1>> P>=0.5 [ target U !target ]