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


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



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

atl "fairnessP4" A G (
			(P1_S4 | P2_S4 | P3_S4) => E F (P4_S1 & P4_S2 & P4_S3)
		);