The answer to the question is, NO, it is not possible to get z in terms of the parameters.
... At least not if, like me, you only have 32 gigabytes of memory.
Your system generates many different branches of conditional cases. Working all of the cases through takes a lot of time to figure out how to proceed, and takes even more memory. I ended up having to kill the process after it started swapping my system.
I suspect you just might be able to get further if you were to remove some of the constraints to positive, as that would reduce the number of different cases to consider. You would then weed through through the results after you had the general framework.