/*
	 * Formula As Typed: [](returndoWork1d1 -> [](! calldoWork1d1))
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !([](returndoWork1d1 -> [](! calldoWork1d1)))
	 * (formalizing violations of the original)
	 */

never {    /* !([](returndoWork1d1 -> [](! calldoWork1d1))) */
T0_init:
	if
	:: (1) -> goto T0_init
	:: ((returndoWork1d1)) -> goto T0_S4
	:: ((calldoWork1d1) && (returndoWork1d1)) -> goto accept_all
	fi;
T0_S4:
	if
	:: (1) -> goto T0_S4
	:: ((calldoWork1d1)) -> goto accept_all
	fi;
accept_all:
	skip
}