inv "fairnessP1" ( P1_stop 
                        => ( (P2_S1 | P3_S1) => (P1_S2 & P1_S3)\
 ) 
                 ); 

inv "fairnessP2" ( P2_stop 
                        => ( (P1_S2 | P3_S2) => (P2_S1 & P2_S3)\
 ) 
                 ); 


inv "fairnessP3" ( P3_stop
			=> ( (P1_S3 | P2_S3) => (P3_S1 & P3_S2) )
		 );