我不明白为什么 Alloy 找不到我的模型的实例

我正在尝试使用合金 4解决Halmos 的握手问题（第 2.3 节）（我的大学课程要求使用合金 4；但是这张问题表不是我的课程作业的一部分，我正尝试将其作为练习来解决）。

这是我提出的模型：

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
}

问题是 Alloy 无法找到 10 s 情况的实例Person，尽管我从问题描述中知道应该有一个 10 Persons 的模型满足我的规范。

run { } for exactly 10 Person给我：

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.

有趣的是，run { } for exactly 8 Person给了我：

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.

并输出如下内容，这似乎与 Halmos 的描述相符（除了Me和 之外，没有两个人MyWife有相同次数的握手）：

同样，run { } for exactly 4 Person正如我所料：

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.

并且run { } for exactly 5 Person未能找到实例（因为我们需要偶数个人员，以将他们匹配为夫妇），正如预期的那样。

那么，为什么 Alloy 在 10 秒内都找不到实例呢Person？是我使用 Alloy 的方式不对，还是我的规范有误？

谢谢，