/*
	 * Formula As Typed: []((returnInputd1 && <>returnInputd2) -> ((! callGetd2) U (callGetd1 || [](!callGetd2))))
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !([]((returnInputd1 && <>returnInputd2) -> ((! callGetd2) U (callGetd1 || [](!callGetd2)))))
	 * (formalizing violations of the original)
	 */

never {    /* !([]((returnInputd1 && <>returnInputd2) -> ((! callGetd2) U (callGetd1 || [](!callGetd2))))) */
T0_init:
	if
	:: (1) -> goto T0_init
	:: (! ((callGetd1)) && (callGetd2) && (returnInputd1)) -> goto T0_S2
	:: (! ((callGetd1)) && (returnInputd1)) -> goto T0_S36
	:: (! ((callGetd1)) && (callGetd2) && (returnInputd1)) -> goto T0_S49
	:: (! ((callGetd1)) && (callGetd2) && (returnInputd1) && (returnInputd2)) -> goto accept_all
	:: (! ((callGetd1)) && (returnInputd1) && (returnInputd2)) -> goto T0_S67
	:: (! ((callGetd1)) && (callGetd2) && (returnInputd1) && (returnInputd2)) -> goto accept_S39
	fi;
accept_S14:
	if
	:: (! ((callGetd1)) && (callGetd2)) -> goto T0_S99
	:: (! ((callGetd1)) && (callGetd2)) -> goto accept_all
	:: (! ((callGetd1))) -> goto T0_S67
	:: (! ((callGetd1)) && (callGetd2)) -> goto T0_S39
	fi;
accept_S39:
	if
	:: (! ((callGetd1)) && (callGetd2)) -> goto accept_all
	:: (! ((callGetd1))) -> goto T0_S67
	:: (! ((callGetd1)) && (callGetd2)) -> goto T0_S39
	fi;
accept_S67:
	if
	:: (! ((callGetd1)) && (callGetd2)) -> goto T0_S99
	:: (! ((callGetd1))) -> goto T0_S67
	:: (! ((callGetd1)) && (callGetd2)) -> goto accept_all
	:: (! ((callGetd1)) && (callGetd2)) -> goto T0_S39
	fi;
accept_S99:
	if
	:: (1) -> goto T0_S99
	:: ((callGetd2)) -> goto accept_all
	fi;
T0_S39:
	if
	:: (! ((callGetd1)) && (callGetd2)) -> goto accept_all
	:: (! ((callGetd1))) -> goto T0_S67
	:: (! ((callGetd1)) && (callGetd2)) -> goto accept_S39
	fi;
T0_S49:
	if
	:: (! ((callGetd1)) && (callGetd2)) -> goto T0_S2
	:: (! ((callGetd1))) -> goto T0_S36
	:: (! ((callGetd1)) && (callGetd2)) -> goto T0_S49
	:: (! ((callGetd1)) && (callGetd2) && (returnInputd2)) -> goto accept_all
	:: (! ((callGetd1)) && (returnInputd2)) -> goto T0_S67
	:: (! ((callGetd1)) && (callGetd2) && (returnInputd2)) -> goto accept_S39
	fi;
T0_S67:
	if
	:: (! ((callGetd1))) -> goto T0_S67
	:: (! ((callGetd1)) && (callGetd2)) -> goto accept_S99
	:: (! ((callGetd1)) && (callGetd2)) -> goto accept_S14
	:: (! ((callGetd1)) && (callGetd2)) -> goto accept_all
	:: (! ((callGetd1)) && (callGetd2)) -> goto accept_S39
	fi;
T0_S99:
	if
	:: (1) -> goto T0_S99
	:: ((callGetd2)) -> goto accept_all
	fi;
T0_S103:
	if
	:: (1) -> goto T0_S103
	:: ((returnInputd2)) -> goto T0_S99
	:: ((callGetd2)) -> goto T0_S2
	:: ((callGetd2) && (returnInputd2)) -> goto accept_all
	fi;
T0_S36:
	if
	:: (! ((callGetd1)) && (callGetd2)) -> goto T0_S103
	:: (! ((callGetd1))) -> goto T0_S36
	:: (! ((callGetd1)) && (callGetd2) && (returnInputd2)) -> goto accept_S99
	:: (! ((callGetd1)) && (callGetd2) && (returnInputd2)) -> goto accept_S67
	:: (! ((callGetd1)) && (callGetd2)) -> goto T0_S2
	:: (! ((callGetd1)) && (callGetd2)) -> goto T0_S49
	:: (! ((callGetd1)) && (callGetd2) && (returnInputd2)) -> goto accept_all
	:: (! ((callGetd1)) && (returnInputd2)) -> goto T0_S67
	:: (! ((callGetd1)) && (callGetd2) && (returnInputd2)) -> goto accept_S39
	fi;
T0_S2:
	if
	:: (1) -> goto T0_S2
	:: ((returnInputd2)) -> goto accept_all
	fi;
accept_all:
	skip
}