What constraint am I missing for this SAT optimization problem?

Question

I'm trying to solve a variation of the bin-packing problem. I have a certain floor space and I wish to place as many boxes as I can without stacking, i.e. if the floor is a 4 x 4 grid and I have one package that is 3 x 3 (A), one that is 3 x 1 (B), and one that is 1 x 4 (C) I could place them as such

$$ B B B C \\ AAAC \\ AAAC \\ AAAC. $$

So to solve this with SAT I have initialised a 4 x 4 grid with bools where each grid point is named $xyp$ where $x$ denotes the current x-value, $y$ the current y-value and $p$ is the package so A, B or C. So for example the bottom left grid point would be denoted 00A, 00B, and 00C in this example. The whole grid would be initialised for each package. \

As for the constraints I've defined them as such:

1. The first constraint is meant to denote where on the grid package A can be placed, and that it can only be placed once and is written as such

Or(And(00A, 01A, 02A, 10A, 11A, 12A, 20A, 21A, 22A),
  And(01A, 02A, 03A, 11A, 12A, 13A, 21A, 22A, 23A),
  And(10A, 11A, 12A, 20A, 21A, 22A, 30A, 31A, 3A0),
  And(11A, 12A, 13A, 21A, 22A, 23A, 31A, 32A, 33A)) 

2. The second constraint is meant to ensure no overlapping between the packages, so it goes through each grid point and ensures that no two packages are placed at the same spot. This is done as such

And(Not(And(00B, 00A)),
    Not(And(01B, 01A)),
    Not(And(02B, 02A)),
    Not(And(03B, 03A)), ... ) 

However, I'm having trouble with that this only works for small problems when I run it with Python (with z3Py if relevant). Once I get to a 14 x 14 grid I'm no longer getting feasible solutions even though they exist. So I'm wondering if I'm missing a constraint or have I formulated myself wrong?