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

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