atl "fairnessP3" A G (
			(P1_Contr | P2_Contr) => E F (P3_Contr)
		);

atl "fairnessP2" A G (
			(P1_Contr | P3_Contr) => E F (P2_Contr)
		);

atl "fairnessP1" A G (
			(P2_Contr | P3_Contr) => E F (P1_Contr)
		);