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

never {    /* !(([](returnInsertd1 -> [](!callInsertd1))) -> ( [](calldoWork1d1 -> [](!calldoWork2d1)))) */
T0_init:
	if
	:: (! ((callInsertd1))) -> goto T0_S171
	:: (! ((returnInsertd1))) -> goto T0_S102
	:: (! ((callInsertd1)) && (calldoWork1d1)) -> goto T0_S141
	:: (! ((returnInsertd1)) && (calldoWork1d1)) -> goto T0_S45
	:: (! ((callInsertd1)) && (calldoWork1d1) && (calldoWork2d1)) -> goto accept_S120
	:: (! ((returnInsertd1)) && (calldoWork1d1) && (calldoWork2d1)) -> goto accept_S33
	fi;
accept_S33:
	if
	:: (! ((callInsertd1))) -> goto T0_S120
	:: (! ((returnInsertd1))) -> goto T0_S33
	fi;
accept_S120:
	if
	:: (! ((callInsertd1))) -> goto T0_S120
	fi;
T0_S33:
	if
	:: (! ((callInsertd1))) -> goto accept_S120
	:: (! ((returnInsertd1))) -> goto accept_S33
	fi;
T0_S45:
	if
	:: (! ((callInsertd1))) -> goto T0_S141
	:: (! ((returnInsertd1))) -> goto T0_S45
	:: (! ((callInsertd1)) && (calldoWork2d1)) -> goto accept_S120
	:: (! ((returnInsertd1)) && (calldoWork2d1)) -> goto accept_S33
	fi;
T0_S102:
	if
	:: (! ((callInsertd1))) -> goto T0_S171
	:: (! ((returnInsertd1))) -> goto T0_S102
	:: (! ((callInsertd1)) && (calldoWork1d1)) -> goto T0_S141
	:: (! ((returnInsertd1)) && (calldoWork1d1)) -> goto T0_S45
	:: (! ((callInsertd1)) && (calldoWork1d1) && (calldoWork2d1)) -> goto accept_S120
	:: (! ((returnInsertd1)) && (calldoWork1d1) && (calldoWork2d1)) -> goto accept_S33
	fi;
T0_S120:
	if
	:: (! ((callInsertd1))) -> goto accept_S120
	fi;
T0_S141:
	if
	:: (! ((callInsertd1))) -> goto T0_S141
	:: (! ((callInsertd1)) && (calldoWork2d1)) -> goto accept_S120
	fi;
T0_S171:
	if
	:: (! ((callInsertd1)) && (calldoWork1d1)) -> goto T0_S141
	:: (! ((callInsertd1))) -> goto T0_S171
	:: (! ((callInsertd1)) && (calldoWork1d1) && (calldoWork2d1)) -> goto accept_S120
	fi;
accept_all:
	skip
}