I cannot understand why Alloy does not find an instance for my model

I am trying to solve Halmos' handshake problem (Section 2.3) using Alloy 4 (I am required to use Alloy 4 for my university course; however this problem sheet is not part of my coursework, I am trying to solve it as practice).

This is the model I came up with:

module halmos

abstract sig Person { shook : set Person }
sig Man extends Person { wife : one Woman }
sig Woman extends Person { husband : one Man }
one sig Me in Man { }
one sig MyWife in Woman { }

fact {
    Me.wife = MyWife
    MyWife.husband = Me
}

// hand-shaking is symmetric
fact { all p : Person | p.shook = shook.p }

// "No one shook his or her own hand"
fact { all p : Person | p not in p.shook }

// "no husband shook his wife’s hand"
// this and symmetricity of shook implies no wife shook her husband's hand
fact { all m : Man | m.wife not in m.shook }

fact monogamy {
    all m : Man, w : Woman |
        // these parens are needed for correct precedence
        (m.wife = w implies w.husband = m)
        and
        (w.husband = m implies m.wife = w)
}

// all distinct persons (other than Me) shook a different number of hands
fact {
    all disj p1,p2 : Person - Me |
        #p1.shook != #p2.shook
}

The problem is that Alloy fails to find an instance for the case with 10 Persons, even though I know from the problem description that there should be a model with 10 Persons satisfying my specification.

run { } for exactly 10 Person gives me:

Executing "Run run$1 for exactly 10 Person"
   Solver=glucose 4.1(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   5762 vars. 440 primary vars. 14101 clauses. 10ms.
   No instance found. Predicate may be inconsistent. 1094ms.

Interestingly, run { } for exactly 8 Person gives me:

Executing "Run run$1 for exactly 8 Person"
   Solver=glucose 4.1(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   3645 vars. 288 primary vars. 8394 clauses. 6ms.
   Instance found. Predicate is consistent. 17ms.

and output like this, which seems to match Halmos' description (no two people -- other than Me and MyWife have the same number of hand-shakees):

similarly, run { } for exactly 4 Person gives me, as expected:

Executing "Run run$1 for exactly 4 Person"
   Solver=glucose 4.1(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   980 vars. 80 primary vars. 1931 clauses. 2ms.
   Instance found. Predicate is consistent. 1ms.

and run { } for exactly 5 Person fails to find an instance (since we need an even number of people, to match them up as couples), as expected.

Why, then, does Alloy fail to find an instance for 10 Persons? Am I using Alloy wrong or is my specification incorrect somehow?

Thanks,

Without looking at your code ... set the int width to 5. At 10 people you cannot handle the cardinality anymore because the default int width is 4: -8-7.