never { /* ! [] ( (p0 /\ p1) -> ((! p1) V (p0 \/ (! p1))) ) */
T1_init:
	if
	:: (1) -> goto T1_init
	:: (p0 && p1) -> goto T0_S2
	fi;
T0_S2:
	if
	:: (p1) -> goto T0_S2
	:: (!p0 && p1) -> goto accept_all
	fi;
accept_all:
	skip
}