I know essentially nothing about Z3 but it seems like there's a potential problem in the code. There's a section headed by the comment "All hits and miss counts

I know essentially nothing about Z3 but it seems like there's a potential problem in the code. There's a section headed by the comment "All hits and miss counts must be positive" followed by a bunch of assertions that those numbers are greater than 0. Isn't it possible that you have 0 hits or misses? I mean, what if your season is short and you only face a couple of lefty pitchers and strike out both times? In any case, I would explain the paradox differently than the author. The author says: "The key to understanding the paradox is that the players did not bat against the same set of pitchers. A batted against 5 lefties and 12 righties; B against 2 and 11." I would say instead that the key to understanding the paradox is to observe that both players are much better when batting against lefties and that player A batted against lefties much more often, both in absolute and relative terms. In other words, A is not as good against lefties as B but he faced a lot more of these comparatively easy pitchers.