/*
	 * Formula As Typed: []  (workCountGRzero && acceptActivePoolGet && !(donew1 || donew2 || donew3) -> <> calldoWork)
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !([]  (workCountGRzero && acceptActivePoolGet && !(donew1 || donew2 || donew3) -> <> calldoWork))
	 * (formalizing violations of the original)
	 */

never {    /* !([]  (workCountGRzero && acceptActivePoolGet && !(donew1 || donew2 || donew3) -> <> calldoWork)) */
T0_init:
	if
	:: (1) -> goto T0_init
	:: (! ((calldoWork)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && (acceptActivePoolGet) && (workCountGRzero)) -> goto accept_S4
	fi;
accept_S4:
	if
	:: (! ((calldoWork))) -> goto T0_S4
	fi;
T0_S4:
	if
	:: (! ((calldoWork))) -> goto accept_S4
	fi;
accept_all:
	skip
}