Alloy assertion on implies command

I try to implement on Alloy the axiomatic system described in a paper on mereology: "Bennett, Having a Part Twice Over, 2013".

I implemented all the axioms, and I thought that if I implemented them correctly, I could assert and check the theorems.

I try to code theorem (T9). This is the theorem in the paper:

And this is how I coded it:

/* (T9) Conditional Reflexivity */
assert conditional_reflexivity {
  all x: Filler |  some z: Slot | z in x.slots implies x in x.parts
}

(Ps(z, x) means that z is a slot of x, and P(x, x) that x is a part of x. I coded both slots and parts as sets.)

However, when I check the assertion, something doesn’t seem to work. I got the following counterexample:

But I do not understand how this is a counterexample to an implication. The premise is not even fulfilled. The only way it makes sense is that it requires that there is a z for every x. In this case, this is for sure a counterexample. In this case, how I can check the theorem?

(I can share the full code if needed.)

As explained by Hovercouch, it was a precedence issue :

you got AE(p impl q) when you wanted A((Ep) impl q)

Adding parentheses fixed the issue.