C auto/C-RW-G+RW-R+RW-G+RW-R+RW-G+RW-R
{
}

P0(int *x0, int *x1, int *gpstart01, int *csend01, int *csend02, int *csend03)
{
	r1 = READ_ONCE(*x0);
	smp_mb();
	smp_store_release(gpstart01, 1);
	smp_mb();
	r60101 = smp_load_acquire(csend01);
	r60201 = smp_load_acquire(csend02);
	r60301 = smp_load_acquire(csend03);
	smp_mb();
	WRITE_ONCE(*x1, 1);
}


P1(int *x1, int *x2, int *gpstart01, int *gpstart02, int *gpstart03, int *csend01)
{
	r50101 = smp_load_acquire(gpstart01);
	r50201 = smp_load_acquire(gpstart02);
	r50301 = smp_load_acquire(gpstart03);
	r1 = READ_ONCE(*x1);
	WRITE_ONCE(*x2, 1);
	smp_store_release(csend01, 1);
}


P2(int *x2, int *x3, int *gpstart02, int *csend01, int *csend02, int *csend03)
{
	r1 = READ_ONCE(*x2);
	smp_mb();
	smp_store_release(gpstart02, 1);
	smp_mb();
	r60102 = smp_load_acquire(csend01);
	r60202 = smp_load_acquire(csend02);
	r60302 = smp_load_acquire(csend03);
	smp_mb();
	WRITE_ONCE(*x3, 1);
}


P3(int *x3, int *x4, int *gpstart01, int *gpstart02, int *gpstart03, int *csend02)
{
	r50102 = smp_load_acquire(gpstart01);
	r50202 = smp_load_acquire(gpstart02);
	r50302 = smp_load_acquire(gpstart03);
	r1 = READ_ONCE(*x3);
	WRITE_ONCE(*x4, 1);
	smp_store_release(csend02, 1);
}


P4(int *x4, int *x5, int *gpstart03, int *csend01, int *csend02, int *csend03)
{
	r1 = READ_ONCE(*x4);
	smp_mb();
	smp_store_release(gpstart03, 1);
	smp_mb();
	r60103 = smp_load_acquire(csend01);
	r60203 = smp_load_acquire(csend02);
	r60303 = smp_load_acquire(csend03);
	smp_mb();
	WRITE_ONCE(*x5, 1);
}


P5(int *x0, int *x5, int *gpstart01, int *gpstart02, int *gpstart03, int *csend03)
{
	r50103 = smp_load_acquire(gpstart01);
	r50203 = smp_load_acquire(gpstart02);
	r50303 = smp_load_acquire(gpstart03);
	r1 = READ_ONCE(*x5);
	WRITE_ONCE(*x0, 1);
	smp_store_release(csend03, 1);
}

exists ( (0:r1=1 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 4:r1=1 /\ 5:r1=1)
 /\ (1:r50101=1 \/ 0:r60101=1) /\ (3:r50102=1 \/ 0:r60201=1)
 /\ (5:r50103=1 \/ 0:r60301=1) /\ (1:r50201=1 \/ 2:r60102=1)
 /\ (3:r50202=1 \/ 2:r60202=1) /\ (5:r50203=1 \/ 2:r60302=1)
 /\ (1:r50301=1 \/ 4:r60103=1) /\ (3:r50302=1 \/ 4:r60203=1)
 /\ (5:r50303=1 \/ 4:r60303=1) )