never {    /* !([](notifyartistse1 -> (!(notifyclienteventa1e2 || notifyclienteventa2e2) U (notifyartistse2 || []!(notifyclienteventa1e2 || notifyclienteventa2e2)))))
 */
T0_init:
	if
	:: (((! ((notifyartistse2)) && ((notifyartistse1) && (notifyclienteventa1e2))) || (! ((notifyartistse2)) && ((notifyartistse1) && (notifyclienteventa2e2))))) -> goto accept_S4
	:: (! ((notifyartistse2)) && (notifyartistse1)) -> goto T0_S3
	:: (((! ((notifyartistse2)) && ((notifyartistse1) && (notifyclienteventa1e2))) || (! ((notifyartistse2)) && ((notifyartistse1) && (notifyclienteventa2e2))))) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_S32:
	if
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto T0_S4
	:: (! ((notifyartistse2))) -> goto T0_S3
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto accept_all
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto T0_S41
	fi;
accept_S41:
	if
	:: (((notifyclienteventa1e2) || (notifyclienteventa2e2))) -> goto accept_all
	:: (1) -> goto T0_S41
	fi;
accept_S4:
	if
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto T0_S4
	:: (! ((notifyartistse2))) -> goto T0_S3
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto accept_all
	fi;
accept_S3:
	if
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto T0_S4
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto accept_all
	:: (! ((notifyartistse2))) -> goto T0_S3
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto T0_S41
	fi;
T0_S41:
	if
	:: (((notifyclienteventa1e2) || (notifyclienteventa2e2))) -> goto accept_all
	:: (1) -> goto T0_S41
	fi;
T0_S4:
	if
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto accept_S4
	:: (! ((notifyartistse2))) -> goto T0_S3
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto accept_all
	fi;
T0_S3:
	if
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto accept_S4
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto accept_all
	:: (! ((notifyartistse2)) && (notifyclienteventa2e2)) -> goto accept_S3
	:: (! ((notifyartistse2)) && (notifyclienteventa1e2)) -> goto accept_S32
	:: (((! ((notifyartistse2)) && (notifyclienteventa1e2)) || (! ((notifyartistse2)) && (notifyclienteventa2e2)))) -> goto accept_S41
	:: (! ((notifyartistse2))) -> goto T0_S3
	fi;
accept_all:
	skip
}