atl "fairnessP1" A G (
                        (P2_S1 | P3_S1) => E F (P1_S3 & P1_S2)
                );
--passed

atl "fairnessP2" A G (
			(P1_S2 | P3_S2) => E F (P2_S1 & P2_S3)
		);
--passed


atl "fairnessP3" A G (
			(P2_S3 | P1_S3) => E F (P3_S1 & P3_S2)
		);
--passed