/*
	 * Formula As Typed: ( ([]( !callstub1)) && ([](! callstub2)) && ([](! callstub3)) ) ->( []  (callExecute -> ((! returnExecute) U (donew1 || donew2 || donew3 || workCountISzero || [] (! returnExecute)))) )
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !(( ([]( !callstub1)) && ([](! callstub2)) && ([](! callstub3)) ) ->( []  (callExecute -> ((! returnExecute) U (donew1 || donew2 || donew3 || workCountISzero || [] (! returnExecute)))) ))
	 * (formalizing violations of the original)
	 */

never {    /* !(( ([]( !callstub1)) && ([](! callstub2)) && ([](! callstub3)) ) ->( []  (callExecute -> ((! returnExecute) U (donew1 || donew2 || donew3 || workCountISzero || [] (! returnExecute)))) )) */
T0_init:
	if
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3))) -> goto T0_init
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (callExecute) && (returnExecute)) -> goto accept_S100
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (callExecute)) -> goto T0_S87
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (callExecute) && (returnExecute)) -> goto accept_S11
	fi;
accept_S11:
	if
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto T0_S100
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero))) -> goto T0_S87
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto T0_S11
	fi;
accept_S74:
	if
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3))) -> goto T0_S74
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && (returnExecute)) -> goto T0_S100
	fi;
accept_S87:
	if
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto T0_S74
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero))) -> goto T0_S87
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto T0_S100
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto T0_S11
	fi;
accept_S100:
	if
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3))) -> goto T0_S100
	fi;
T0_S11:
	if
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_S100
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero))) -> goto T0_S87
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_S11
	fi;
T0_S74:
	if
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3))) -> goto T0_S74
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && (returnExecute)) -> goto accept_S100
	fi;
T0_S87:
	if
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_S74
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero))) -> goto T0_S87
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_S87
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_S100
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3)) && ! ((donew1)) && ! ((donew2)) && ! ((donew3)) && ! ((workCountISzero)) && (returnExecute)) -> goto accept_S11
	fi;
T0_S100:
	if
	:: (! ((callstub1)) && ! ((callstub2)) && ! ((callstub3))) -> goto accept_S100
	fi;
accept_all:
	skip
}